[isabelle-dev] NEWS: command 'define'

[Makarius]

*** Isar ***

* Command 'define' introduces a local (non-polymorphic) definition, with
optional abstraction over local parameters. The syntax resembles
'definition' and 'obtain'. It fits better into the Isar language than
old 'def', which is now a legacy feature.


This refers to Isabelle/df83a961d3a8.

In Isabelle/eb4ddd18d635 I have already eliminated the old 'def' command 
from the applications in the repository. As I've eliminated most lambdas, 
preferring explicit arguments "f x y = t" instead, there are occasional 
uses of the abs_def attribute to help unfolding/unfold or simp.

Maybe unfolding/unfold should always apply abs_def to its arguments, with 
an option to disable that for backwards compatibility. This has the 
potential to avoid surprises, when nothing is unfolded due to lack of 
arguments in the application. It would make "unfold" more a device to 
unfold definitions, instead of a minimal version of the Simplifier.


 	Makarius