NEWS
changeset 48205 09c2a3d9aa22
parent 48171 28a6d67c93f0
child 48206 937b53a339f0
--- a/NEWS	Thu Jul 05 22:17:57 2012 +0200
+++ b/NEWS	Fri Jul 06 16:20:54 2012 +0200
@@ -13,6 +13,15 @@
 in old "ref" manual.
 
 
+*** Pure ***
+
+* Discontinued obsolete attribute "COMP".  Potential INCOMPATIBILITY,
+use regular rule composition via "OF" / "THEN", or explicit proof
+structure instead.  Note that Isabelle/ML provides a variety of
+operators like COMP, INCR_COMP, COMP_INCR, which need to be applied
+with some care where this is really required.
+
+
 *** Document preparation ***
 
 * Default for \<euro> is now based on eurosym package, instead of