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