# HG changeset patch
# User wenzelm
# Date 1119462500 -7200
# Node ID 09f7a953d2d67797fa7cff1398129403e30c547c
# Parent  77e7fd18b7852ab3e9414437c4ee6d2fa88ef217
* Pure: the Isar proof context type is already defined early in Pure
  as Context.proof;

diff -r 77e7fd18b785 -r 09f7a953d2d6 NEWS
--- 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