--- a/NEWS Tue Oct 16 23:02:14 2001 +0200
+++ b/NEWS Wed Oct 17 18:50:49 2001 +0200
@@ -121,19 +121,23 @@
*** General ***
-* Meta-level proof terms (by Stefan Berghofer), see also ref manual;
-
-* new token syntax "num" for plain numerals (without "#" of "xnum");
-potential INCOMPATIBILITY, since -0, -1 etc. are now separate tokens,
-so expressions involving minus need to be spaced properly;
-
-* Classical reasoner: renamed addaltern to addafter, addSaltern to
+* kernel: meta-level proof terms (by Stefan Berghofer), see also ref
+manual;
+
+* classical reasoner: renamed addaltern to addafter, addSaltern to
addSafter;
+* syntax: new token syntax "num" for plain numerals (without "#" of
+"xnum"); potential INCOMPATIBILITY, since -0, -1 etc. are now separate
+tokens, so expressions involving minus need to be spaced properly;
+
* syntax: support non-oriented infixes;
-* print modes "type_brackets" and "no_type_brackets" control output of
-nested => (types); the default behavior is "brackets";
+* syntax: print modes "type_brackets" and "no_type_brackets" control
+output of nested => (types); the default behavior is "type_brackets";
+
+* syntax: builtin parse translation for "_constify" turns valued
+tokens into AST constants;
* system: support Poly/ML 4.1.1 (now able to manage large heaps);