diff -r 144d94446378 -r 216a839841bc NEWS
--- 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