florian.haftmann at informatik.tu-muenchen.de
Thu Nov 22 18:38:18 CET 2012
> The latter aspect is gradually being superseded by the ROOT setup: it
> tells which collection of theories (without merging) contribute to a
> session. In the next round of the reforms the Prover IDE should be able
> to import all of them in interactive mode, like build does in batch mode.
I'm looking forward to that since a constantly stumble over sessions
which are difficult to maintain interactively.
> I can't say anything specific, only point to the 2-3 FIXMEs in
> Isabelle/bc82d25af543 in this respect (in src/HOL/ROOT and
This is on my agenda, but I have found no time yet to have a closer look
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 261 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev