diff -r 4b2eccaec3f6 -r e7ea35b41e2d NEWS
--- a/NEWS	Wed Mar 14 11:10:10 2012 +0100
+++ b/NEWS	Wed Mar 14 11:45:16 2012 +0100
@@ -371,6 +371,12 @@
 
 *** ML ***
 
+* Local_Theory.define no longer hard-wires default theorem name
+"foo_def": definitional packages need to make this explicit, and may
+choose to omit theorem bindings for definitions by using
+Binding.empty/Attrib.empty_binding.  Potential INCOMPATIBILITY for
+derived definitional packages.
+
 * Renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in
 conformance with similar operations in structure Term and Logic.