[isabelle-dev] NEWS

Makarius makarius at sketis.net
Fri Jul 20 19:12:39 CEST 2007


* Theory loader: be more serious about observing the static theory
header specifications (including optional directories), but not the
accidental file locations of previously successful loads.  Potential
INCOMPATIBILITY, may need to refine theory headers.

* Theory loader: optional support for content-based file
identification, instead of the traditional scheme of full physical
path plus date stamp; configured by the ISABELLE_FILE_IDENT setting,
(cf. the system manual).  The new scheme allows to work with
non-finished theories in persistent session images, such that source
files may be moved later on without requiring reloads.




More information about the isabelle-dev mailing list