--- a/NEWS Sat Mar 29 19:24:57 2008 +0100
+++ b/NEWS Sat Mar 29 22:55:49 2008 +0100
@@ -29,8 +29,9 @@
*** Pure ***
-* Eliminated destructive theorem database. Potential INCOMPATIBILITY,
-really need to observe linear functional update of theories.
+* Eliminated destructive theorem database, simpset, claset, and
+clasimpset. Potential INCOMPATIBILITY, really need to observe linear
+update of theories within ML code.
* Commands 'use' and 'ML' are now purely functional, operating on
theory/local_theory. Removed former 'ML_setup' (on theory), use 'ML'