NEWS
changeset 13587 659813a3f879
parent 13570 0d6a0dce3ba3
child 13613 531f1f524848
     1.1 --- a/NEWS	Thu Sep 26 10:51:58 2002 +0200
     1.2 +++ b/NEWS	Thu Sep 26 10:56:20 2002 +0200
     1.3 @@ -42,6 +42,9 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* function INCOMPATIBILITIES: Pi-sets have been redefined and moved from main 
     1.8 +HOL to Library/FuncSet; constant "Fun.op o" is now called "Fun.comp";
     1.9 +
    1.10  * 'typedef' command has new option "open" to suppress the set
    1.11  definition;
    1.12  
    1.13 @@ -71,6 +74,8 @@
    1.14  
    1.15  * the simplifier trace now shows the names of the applied rewrite rules
    1.16  
    1.17 +* GroupTheory: converted to Isar theories, using locales with implicit structures;
    1.18 +
    1.19  * Real/HahnBanach: updated and adapted to locales;
    1.20  
    1.21