[isabelle-dev] NEWS: isabelle imports

[Makarius]

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