--- a/NEWS Thu Sep 26 10:51:58 2002 +0200
+++ b/NEWS Thu Sep 26 10:56:20 2002 +0200
@@ -42,6 +42,9 @@
*** HOL ***
+* function INCOMPATIBILITIES: Pi-sets have been redefined and moved from main
+HOL to Library/FuncSet; constant "Fun.op o" is now called "Fun.comp";
+
* 'typedef' command has new option "open" to suppress the set
definition;
@@ -71,6 +74,8 @@
* the simplifier trace now shows the names of the applied rewrite rules
+* GroupTheory: converted to Isar theories, using locales with implicit structures;
+
* Real/HahnBanach: updated and adapted to locales;