NEWS
changeset 16547 09f7a953d2d6
parent 16506 b2687ce38433
child 16563 a92f96951355
     1.1 --- a/NEWS	Wed Jun 22 19:44:12 2005 +0200
     1.2 +++ b/NEWS	Wed Jun 22 19:48:20 2005 +0200
     1.3 @@ -453,6 +453,11 @@
     1.4  etc.) as well as the sign field in Thm.rep_thm etc. have been retained
     1.5  for convenience -- they merely return the theory.
     1.6  
     1.7 +* Pure: the Isar proof context type is already defined early in Pure
     1.8 +as Context.proof (note that ProofContext.context and Proof.context are
     1.9 +aliases, where the latter is the preferred name).  This enables other
    1.10 +Isabelle components to refer to that type even before Isar is present.
    1.11 +
    1.12  * Pure/sign/theory: discontinued named name spaces (i.e. classK,
    1.13  typeK, constK, axiomK, oracleK), but provide explicit operations for
    1.14  any of these kinds.  For example, Sign.intern typeK is now