On 12/09/2019 15:04, Makarius wrote:
> *** General ***
>
> * Session ROOT files need to specify explicit 'directories' for import
> of theory files. Directories cannot be shared by different sessions.
> (Recall that import of theories from other sessions works via
> session-qualified theory names, together with suitable 'sessions'
> declarations in the ROOT.)
An important consequence is that a theory file gets a unique
session-qualified name, without accidental multiplication of theories
that is occasionally seen in applications.
Thus by forcing users to clean up their session/theory arrangement, some
applications might become faster without further ado. (In the past 2
years, I've cleaned up such situations several times in AFP, and it is
all fine in AFP/98320942654a).
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
