--- a/NEWS Sat Mar 29 13:03:09 2008 +0100
+++ b/NEWS Sat Mar 29 19:13:58 2008 +0100
@@ -29,6 +29,14 @@
*** Pure ***
+* Eliminated destructive theorem database. Potential INCOMPATIBILITY,
+really need to observe linear functional update of theories.
+
+* Commands 'use' and 'ML' are now purely functional, opearing on
+theory/local_theory. Removed former 'ML_setup' (on theory), use 'ML'
+instead. Added 'ML_val' as mere diagnostic replacement for 'ML'.
+INCOMPATIBILITY.
+
* Eliminated theory ProtoPure. Potential INCOMPATIBILITY.
* Command 'setup': discontinued implicit version.