[isabelle-dev] NEWS: command 'define'
makarius at sketis.net
Mon Apr 25 21:57:25 CEST 2016
*** 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.
More information about the isabelle-dev