--- a/NEWS Sun May 18 16:19:48 2008 +0200
+++ b/NEWS Sun May 18 17:03:14 2008 +0200
@@ -76,7 +76,10 @@
clasimpset. Potential INCOMPATIBILITY, really need to observe linear
update of theories within ML code.
-* Eliminated theory ProtoPure. Potential INCOMPATIBILITY.
+* Eliminated theory ProtoPure and CPure, leaving just one Pure theory.
+INCOMPATIBILITY, object-logics depending on former Pure require
+additional setup PureThy.old_appl_syntax_setup; object-logics
+depending on former CPure need to refer to Pure.
* Commands 'use' and 'ML' are now purely functional, operating on
theory/local_theory. Removed former 'ML_setup' (on theory), use 'ML'