* HOL: bounded abstraction now uses syntax "%" / "\<lambda>" instead
of "lam" -- INCOMPATIBILITY;

--- 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 ***