*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Kind of generic lemmas: possible?*From*: Christian Sternagel <c-sterna at jaist.ac.jp>*Date*: Mon, 06 Aug 2012 12:03:20 +0900*In-reply-to*: <op.willhltkule2fv@douda-yannick>*References*: <op.willhltkule2fv@douda-yannick>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:14.0) Gecko/20120717 Thunderbird/14.0

On 08/06/2012 11:35 AM, Yannick Duchêne (Hibou57) wrote:

Hi people out there, Here is a naive attempt I've just made for testing. It is self explanatory: lemma obligation: "f x y ⟹ f y x" sorry fun equal :: "nat ⇒ nat ⇒ bool" where "equal x y = (x = y)" thm obligation [where f = equal] lemma equal_obligation: obligation [where f = equal] The “thm” line is OK, but not the last lemma. Is this just stupid in an Isabelle context or is there another way to achieve the same purpose?

Try lemmas equal_obligation = obligation [where f = equal] (Note the trailing 's' in 'lemmas'.)

cheers chris

**Follow-Ups**:**Re: [isabelle] Kind of generic lemmas: possible?***From:*Yannick Duchêne (Hibou57)

**References**:**[isabelle] Kind of generic lemmas: possible?***From:*Yannick Duchêne (Hibou57)

- Previous by Date: [isabelle] Kind of generic lemmas: possible?
- Next by Date: Re: [isabelle] Kind of generic lemmas: possible?
- Previous by Thread: [isabelle] Kind of generic lemmas: possible?
- Next by Thread: Re: [isabelle] Kind of generic lemmas: possible?
- Cl-isabelle-users August 2012 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