*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Isabelle2016-1-RC3 available for testing: new define command*From*: Christian Sternagel <c.sternagel at gmail.com>*Date*: Fri, 25 Nov 2016 11:03:41 +0100*In-reply-to*: <26df9858-15fc-10bb-908b-a5cf02cc6dd2@sketis.net>*References*: <26df9858-15fc-10bb-908b-a5cf02cc6dd2@sketis.net>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:45.0) Gecko/20100101 Thunderbird/45.4.0

Dear Makarius, I was replacing some 'def "f == %x. P x"' by the new 'define' command and have two comments: 1) For 'definition' the constant name and the 'where' can be dropped, e.g., definition "f = ..." I do this a lot, because definition f where "f = ..." seems a bit silly (I mostly do this whenever I deem the type of "f" to be so obvious that I do not want to state it explicitly). I would like to have the same option also for 'define'. 2) I would have guessed (but reading isar-ref showed me otherwise) that define f where "f x = P x" is (almost) the same as define f where "f = (%x. P x)" but for that I need define f where "f x = P x" for x While this is consistent with 'have ... if ... for ...' it is different from what 'definition' does, and for some reason I was expecting to behave 'define' very similar to 'definition' (it might have been the name ;)). Is there a specific reason that arguments of the left-hand side of 'define' are not meta-all-quantified implicitly? cheers chris On 11/22/2016 10:36 AM, Makarius wrote: > Dear Isabelle users, > > after more than 2 weeks, here is the next release candidate for > Isabelle2016-1 (December 2016): > http://isabelle.in.tum.de/website-Isabelle2016-1-RC3 -- see also > http://sketis.net/2016/release-candidates-for-isabelle2016-1. > > More fine points have been consolidated. A component for the new > experimental Nunchaku tool has been included. > > > The corresponding repository versions of Isabelle and AFP are > https://bitbucket.org/isabelle_project/isabelle-release/commits/8bf3d0553c35 > > and https://bitbucket.org/isa-afp/afp-devel/commits/1a3901597f0f > > It is also possible to follow nightly development snapshots from > http://isabelle.in.tum.de/devel although they might be somewhat erratic. > > > At this stage, Isabelle release candidates are already sufficiently > consolidated to be ready for everyday use. Adapting your applications > now gives a unique chance for feedback before the release is finalized. > > When discussing problems, observations, suggestions, etc. the mail > subject line should be changed to something informative, and the > particular Isabelle version given in the message body. > > > Makarius >

**Follow-Ups**:

**References**:**[isabelle] Isabelle2016-1-RC3 available for testing***From:*Makarius

- Previous by Date: Re: [isabelle] Isabelle2016-1-RC3 available for testing
- Next by Date: Re: [isabelle] Isabelle2016-1-RC3 available for testing: new define command
- Previous by Thread: Re: [isabelle] Isabelle2016-1-RC3 available for testing
- Next by Thread: Re: [isabelle] Isabelle2016-1-RC3 available for testing: new define command
- Cl-isabelle-users November 2016 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list