*** System ***
* Command-line tool "isabelle imports" helps to maintain theory imports
wrt. session structure. Examples:
isabelle imports -I -a
isabelle imports -U -a
isabelle imports -M -a -d '~~/src/Benchmarks'
This refers to Isabelle/c556c09765dd. It is an emerging tool to help
sorting out theory imports from other sessions. So far, I have applied
mainly the operations -I and -M to clarify some ROOT entries, e.g. to
avoid multiple loading of theory sources (like
src/HOL/Library/Multiset.thy).
When the situation has become sufficiently clear -- especially the
situation in AFP -- it should be possible to make one big sweep with
"isabelle imports -U" to have qualified theory imports everywhere. That
will be also the point of no return, but there is no need to rush into that.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
