*** 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

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.

isabelle-dev mailing list

Reply via email to