NEWS
changeset 12312 f0f06950820d
parent 12280 fc7e3f01bc40
child 12335 db4d5f498742
     1.1 --- a/NEWS	Wed Nov 28 00:46:26 2001 +0100
     1.2 +++ b/NEWS	Wed Nov 28 23:27:35 2001 +0100
     1.3 @@ -32,7 +32,7 @@
     1.4  
     1.5  *** Isar ***
     1.6  
     1.7 -* improved proof by cases and induction:
     1.8 +* Pure/Provers: improved proof by cases and induction;
     1.9    - 'case' command admits impromptu naming of parameters (such as
    1.10      "case (Suc n)");
    1.11    - 'induct' method divinates rule instantiation from the inductive
    1.12 @@ -106,6 +106,9 @@
    1.13  chance to get type-inference of the arguments right (this is
    1.14  especially important for locales);
    1.15  
    1.16 +* Pure: "sorry" no longer requires quick_and_dirty in interactive
    1.17 +mode;
    1.18 +
    1.19  * Provers: 'simplified' attribute may refer to explicit rules instead
    1.20  of full simplifier context; 'iff' attribute handles conditional rules;
    1.21  
    1.22 @@ -238,7 +241,13 @@
    1.23  separate tokens, so expressions involving minus need to be spaced
    1.24  properly;
    1.25  
    1.26 -* Pure/syntax: support non-oriented infixes;
    1.27 +* Pure/syntax: support non-oriented infixes, using keyword "infix"
    1.28 +rather than "infixl" or "infixr";
    1.29 +
    1.30 +* Pure/syntax: concrete syntax for dummy type variables admits genuine
    1.31 +sort constraint specifications in type inference; e.g. "x::_::foo"
    1.32 +ensures that the type of "x" is of sort "foo" (but not necessarily a
    1.33 +type variable);
    1.34  
    1.35  * Pure/syntax: print modes "type_brackets" and "no_type_brackets"
    1.36  control output of nested => (types); the default behavior is