* Isar/Pure: "sorry" no longer requires quick_and_dirty in interactive mode;
* Pure/syntax: "x::_::foo" sort constraints;

--- a/NEWS	Wed Nov 28 00:46:26 2001 +0100
+++ b/NEWS	Wed Nov 28 23:27:35 2001 +0100
@@ -32,7 +32,7 @@
 
 *** Isar ***
 
-* improved proof by cases and induction:
+* Pure/Provers: improved proof by cases and induction;
   - 'case' command admits impromptu naming of parameters (such as
     "case (Suc n)");
   - 'induct' method divinates rule instantiation from the inductive
@@ -106,6 +106,9 @@
 chance to get type-inference of the arguments right (this is
 especially important for locales);
 
+* Pure: "sorry" no longer requires quick_and_dirty in interactive
+mode;
+
 * Provers: 'simplified' attribute may refer to explicit rules instead
 of full simplifier context; 'iff' attribute handles conditional rules;
 
@@ -238,7 +241,13 @@
 separate tokens, so expressions involving minus need to be spaced
 properly;
 
-* Pure/syntax: support non-oriented infixes;
+* Pure/syntax: support non-oriented infixes, using keyword "infix"
+rather than "infixl" or "infixr";
+
+* Pure/syntax: concrete syntax for dummy type variables admits genuine
+sort constraint specifications in type inference; e.g. "x::_::foo"
+ensures that the type of "x" is of sort "foo" (but not necessarily a
+type variable);
 
 * Pure/syntax: print modes "type_brackets" and "no_type_brackets"
 control output of nested => (types); the default behavior is