diff -r 0f339348df0e -r 659813a3f879 NEWS
--- 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;