[isabelle-dev] NEWS: isabelle imports

Makarius makarius at sketis.net
Mon Apr 24 16:06:27 CEST 2017

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


More information about the isabelle-dev mailing list