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-...@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
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
