--- a/NEWS Mon Dec 10 19:14:56 2001 +0100
+++ b/NEWS Mon Dec 10 20:57:44 2001 +0100
@@ -152,7 +152,6 @@
'induct_tac', 'case_tac', and 'typecheck' (with attribute 'TC');
-
*** HOL ***
* HOL: moved over to sane numeral syntax; the new policy is as
@@ -228,13 +227,16 @@
* HOL: syntax translations now work properly with numerals and records
expressions;
-* HOL/GroupTheory: group theory examples including Sylow's theorem, by
-Florian Kammüller;
+* HOL: bounded abstraction now uses syntax "%" / "\<lambda>" instead
+of "lam" -- INCOMPATIBILITY;
* HOL: got rid of some global declarations (potential INCOMPATIBILITY
for ML tools): const "()" renamed "Product_Type.Unity", type "unit"
renamed "Product_Type.unit";
+* HOL/GroupTheory: group theory examples including Sylow's theorem, by
+Florian Kammüller;
+
*** HOLCF ***