[isabelle-dev] NEWS: basic definitions

[Makarius]

* 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
undocumented feature.)

* Local_Theory.define no longer hard-wires default theorem name
"foo_def", but retains the binding as given.  If that is Binding.empty
/ Attrib.empty_binding, the result is not registered as user-level
fact.  The Local_Theory.define_internal variant allows to specify a
non-empty name (used for the foundation in the background theory),
while omitting the fact binding in the user-context.  Potential
INCOMPATIBILITY for derived definitional packages: need to specify
naming policy for primitive definitions more explicitly.


This refers to Isabelle/95bd95addb24.

The motivation for the change of 'definition' was twofold:

   (1) raw_def thms occasionally get in the way of other tools;

   (2) extra copy of def thms need to be managed by the target 
infrastructure explicitly, slowing down big locale applications 
unnecessarily.

As a general rule of thumb, it is better to reproduce results on the spot 
(cf. abs_def by Stefan Berghofer above), instead of storing them 
permanently.  (Our theory context are getting quite large, which is where 
all the GBs are going.)


Authors of definitional packages might consider 
Local_Theory.define_internal for other reasons, e.g. to hide internal 
foundations from the end-user: thus primitive def axioms can be made 
inaccessible in the thm name space.

So far, I've tried to retain the behaviour of existing packages 
faithfully in this respect, without any reforms yet.


 	Makarius