NEWS
changeset 16456 451f1c46d4ca
parent 16373 9d020423093b
child 16506 b2687ce38433
     1.1 --- a/NEWS	Fri Jun 17 18:33:40 2005 +0200
     1.2 +++ b/NEWS	Fri Jun 17 18:33:41 2005 +0200
     1.3 @@ -424,6 +424,32 @@
     1.4  the original result when interning again, even if there is an overlap
     1.5  with earlier declarations.
     1.6  
     1.7 +* Pure/TheoryDataFun: change of the argument structure; 'prep_ext' is
     1.8 +now 'extend', and 'merge' gets an additional Pretty.pp argument
     1.9 +(useful for printing error messages).  INCOMPATIBILITY.
    1.10 +
    1.11 +* Pure: major reorganization of the theory context.  Type Sign.sg and
    1.12 +Theory.theory are now identified, referring to the universal
    1.13 +Context.theory (see Pure/context.ML).  Actual signature and theory
    1.14 +content is managed as theory data.  The old code and interfaces were
    1.15 +spread over many files and structures; the new arrangement introduces
    1.16 +considerable INCOMPATIBILITY to gain more clarity:
    1.17 +
    1.18 +  Context -- theory management operations (name, identity, inclusion,
    1.19 +    parents, ancestors, merge, etc.), plus generic theory data;
    1.20 +
    1.21 +  Sign -- logical signature and syntax operations (declaring consts,
    1.22 +    types, etc.), plus certify/read for common entities;
    1.23 +
    1.24 +  Theory -- logical theory operations (stating axioms, definitions,
    1.25 +    oracles), plus a copy of logical signature operations (consts,
    1.26 +    types, etc.); also a few basic management operations (Theory.copy,
    1.27 +    Theory.merge, etc.)
    1.28 +
    1.29 +The most basic sign_of operations (Theory.sign_of, Thm.sign_of_thm
    1.30 +etc.) as well as the sign field in Thm.rep_thm etc. have been retained
    1.31 +for convenience -- they merely return the theory.
    1.32 +
    1.33  * Pure/sign/theory: discontinued named name spaces (i.e. classK,
    1.34  typeK, constK, axiomK, oracleK), but provide explicit operations for
    1.35  any of these kinds.  For example, Sign.intern typeK is now