--- a/NEWS Sat Mar 17 11:35:18 2012 +0100
+++ b/NEWS Sat Mar 17 11:57:03 2012 +0100
@@ -48,6 +48,10 @@
*** Pure ***
+* Command 'definition' no longer exports the foundational "raw_def"
+into the user context. Minor INCOMPATIBILITY, may use the regular
+"def" result with attribute "abs_def" to imitate the old version.
+
* Attribute "abs_def" turns an equation of the form "f x y == t" into
"f == %x y. t", which ensures that "simp" or "unfold" steps always
expand it. This also works for object-logic equality. (Formerly