1.1 --- a/NEWS	Sat Mar 17 12:37:32 2012 +0000
     1.2 +++ b/NEWS	Sat Mar 17 16:13:41 2012 +0100
     1.3 @@ -390,10 +390,13 @@
     1.4  header declaration; it can be passed to Outer_Syntax.command etc.
     1.5  
     1.6  * Local_Theory.define no longer hard-wires default theorem name
     1.7 -"foo_def": definitional packages need to make this explicit, and may
     1.8 -choose to omit theorem bindings for definitions by using
     1.9 -Binding.empty/Attrib.empty_binding.  Potential INCOMPATIBILITY for
    1.10 -derived definitional packages.
    1.11 +"foo_def", but retains the binding as given.  If that is Binding.empty
    1.12 +/ Attrib.empty_binding, the result is not registered as user-level
    1.13 +fact.  The Local_Theory.define_internal variant allows to specify a
    1.14 +non-empty name (used for the foundation in the background theory),
    1.15 +while omitting the fact binding in the user-context.  Potential
    1.16 +INCOMPATIBILITY for derived definitional packages: need to specify
    1.17 +naming policy for primitive definitions more explicitly.
    1.18  
    1.19  * Renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in
    1.20  conformance with similar operations in structure Term and Logic.