# HG changeset patch
# User wenzelm
# Date 1211122994 -7200
# Node ID ebbaa935eae06249b50dfcff6769ea5888e1c53b
# Parent  3a3816ca44bb79d2b978d1ebec9662e1a1febdcf
* Eliminated theory ProtoPure and CPure, leaving just one Pure theory.

diff -r 3a3816ca44bb -r ebbaa935eae0 NEWS
--- 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'