NEWS
changeset 11817 875ee0c20da2
parent 11814 1de4a3321976
child 11842 b903d3dabbe2
     1.1 --- a/NEWS	Tue Oct 16 23:02:14 2001 +0200
     1.2 +++ b/NEWS	Wed Oct 17 18:50:49 2001 +0200
     1.3 @@ -121,19 +121,23 @@
     1.4  
     1.5  *** General ***
     1.6  
     1.7 -* Meta-level proof terms (by Stefan Berghofer), see also ref manual;
     1.8 -
     1.9 -* new token syntax "num" for plain numerals (without "#" of "xnum");
    1.10 -potential INCOMPATIBILITY, since -0, -1 etc. are now separate tokens,
    1.11 -so expressions involving minus need to be spaced properly;
    1.12 -
    1.13 -* Classical reasoner: renamed addaltern to addafter, addSaltern to
    1.14 +* kernel: meta-level proof terms (by Stefan Berghofer), see also ref
    1.15 +manual;
    1.16 +
    1.17 +* classical reasoner: renamed addaltern to addafter, addSaltern to
    1.18  addSafter;
    1.19  
    1.20 +* syntax: new token syntax "num" for plain numerals (without "#" of
    1.21 +"xnum"); potential INCOMPATIBILITY, since -0, -1 etc. are now separate
    1.22 +tokens, so expressions involving minus need to be spaced properly;
    1.23 +
    1.24  * syntax: support non-oriented infixes;
    1.25  
    1.26 -* print modes "type_brackets" and "no_type_brackets" control output of
    1.27 -nested => (types); the default behavior is "brackets";
    1.28 +* syntax: print modes "type_brackets" and "no_type_brackets" control
    1.29 +output of nested => (types); the default behavior is "type_brackets";
    1.30 +
    1.31 +* syntax: builtin parse translation for "_constify" turns valued
    1.32 +tokens into AST constants;
    1.33  
    1.34  * system: support Poly/ML 4.1.1 (now able to manage large heaps);
    1.35