[isabelle-dev] NEWS: command 'define'

[Florian Haftmann]

Very nice!

Am 25.04.2016 um 21:57 schrieb 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
> 
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 836 bytes
Desc: OpenPGP digital signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20160505/babcbceb/attachment.asc>