--- 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.