NEWS
changeset 12457 cbfc53e45476
parent 12405 9b16f99fd7b9
child 12467 b5630a4ea5d8
     1.1 --- a/NEWS	Mon Dec 10 19:14:56 2001 +0100
     1.2 +++ b/NEWS	Mon Dec 10 20:57:44 2001 +0100
     1.3 @@ -152,7 +152,6 @@
     1.4  'induct_tac', 'case_tac', and 'typecheck' (with attribute 'TC');
     1.5  
     1.6  
     1.7 -
     1.8  *** HOL ***
     1.9  
    1.10  * HOL: moved over to sane numeral syntax; the new policy is as
    1.11 @@ -228,13 +227,16 @@
    1.12  * HOL: syntax translations now work properly with numerals and records
    1.13  expressions;
    1.14  
    1.15 -* HOL/GroupTheory: group theory examples including Sylow's theorem, by
    1.16 -Florian Kammüller;
    1.17 +* HOL: bounded abstraction now uses syntax "%" / "\<lambda>" instead
    1.18 +of "lam" -- INCOMPATIBILITY;
    1.19  
    1.20  * HOL: got rid of some global declarations (potential INCOMPATIBILITY
    1.21  for ML tools): const "()" renamed "Product_Type.Unity", type "unit"
    1.22  renamed "Product_Type.unit";
    1.23  
    1.24 +* HOL/GroupTheory: group theory examples including Sylow's theorem, by
    1.25 +Florian Kammüller;
    1.26 +
    1.27  
    1.28  *** HOLCF ***
    1.29