> 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
> src/HOL/Library/Library.thy).
This is on my agenda, but I have found no time yet to have a closer look
at it.
Florian
--
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
