*** General *** * Theory names are qualified by the session name that they belong to. This affects imports, but not the theory name space prefix (which is just the theory base name as before).
In order to import theories from other sessions, the ROOT file format provides a new 'sessions' keyword. In contrast, a theory that is imported in the old-fashioned manner via an explicit file-system path belongs to the current session, and might cause theory name confusion later on. Theories that are imported from other sessions are excluded from the current session document. The command-line tool "isabelle imports" helps to update theory imports. Properly qualified imports allow the Prover IDE to process arbitrary theory hierarchies independently of the underlying logic session image (e.g. option "isabelle jedit -l"), but the directory structure needs to be known in advance (e.g. option "isabelle jedit -d" or a line in the file $ISABELLE_HOME_USER/ROOTS). This refers to Isabelle/1a73ad1c06dd. It is the outcome of struggling with many unexpected problems and corner cases. We have quite some complexity (or complication) in AFP, with various adhoc sessions with overlapping sources. Hopefully it now works smoothly. In any case, the coming weeks before the Isabelle2017 release are there to consolidate it beyond doubt. Makarius _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev