NEWS
changeset 23888 babe337cce2d
parent 23881 851c74f1bb69
child 23889 1794f405eacc
     1.1 --- a/NEWS	Fri Jul 20 19:09:11 2007 +0200
     1.2 +++ b/NEWS	Fri Jul 20 19:10:05 2007 +0200
     1.3 @@ -24,6 +24,18 @@
     1.4  'fun', 'help', 'if') are now keywords.  INCOMPATIBILITY, use double
     1.5  quotes.
     1.6  
     1.7 +* Theory loader: be more serious about observing the static theory
     1.8 +header specifications (including optional directories), but not the
     1.9 +accidental file locations of previously successful loads.  Potential
    1.10 +INCOMPATIBILITY, may need to refine theory headers.
    1.11 +
    1.12 +* Theory loader: optional support for content-based file
    1.13 +identification, instead of the traditional scheme of full physical
    1.14 +path plus date stamp; configured by the ISABELLE_FILE_IDENT setting,
    1.15 +(cf. the system manual).  The new scheme allows to work with
    1.16 +non-finished theories in persistent session images, such that source
    1.17 +files may be moved later on without requiring reloads.
    1.18 +
    1.19  * Legacy goal package: reduced interface to the bare minimum required
    1.20  to keep existing proof scripts running.  Most other user-level
    1.21  functions are now part of the OldGoals structure, which is *not* open