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

On 25/11/16 11:03, Christian Sternagel wrote: > > 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? 'define' is a proof context element and 'definition' a theory specification element. There are different policies for variable binding: the theory language allows more sloppiness. There are some more differences. In some sense, 'define' is not a really a definition, because Hindley-Milner polymorphism is lacking. It might be better to think of 'define' as a variant of 'obtain' -- the syntax is also quite close. Makarius

**Follow-Ups**:**Re: [isabelle] Isabelle2016-1-RC3 available for testing: new define command***From:*Johannes Hölzl

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

**Re: [isabelle] Isabelle2016-1-RC3 available for testing: new define command***From:*Christian Sternagel

- Previous by Date: Re: [isabelle] Isabelle2016-1-RC3 available for testing: new define command
- 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: new define command
- 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