*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Schematic vars or universal bound vars in theorem?*From*: Gottfried Barrow <gottfried.barrow at gmx.com>*Date*: Wed, 18 Jul 2012 12:31:13 -0500*In-reply-to*: <485EE543-83A4-4296-A6EB-2FCC934E3825@cam.ac.uk>*References*: <5006C3EC.50004@gmx.com> <485EE543-83A4-4296-A6EB-2FCC934E3825@cam.ac.uk>*User-agent*: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:11.0) Gecko/20120312 Thunderbird/11.0

On 7/18/2012 12:02 PM, John Wickerson wrote:

I think you should state the theorem without the \<forall>, because it makes it easier to use the theorem later on. For instance, you can say... using SigmaE_is_unique[of "foo"]...to obtain SigmaE_is_unique in the case when u is foo. You can't do this so easily when you have the \<forall> there. john

John,

Thanks, GB

**Follow-Ups**:

**References**:**[isabelle] Schematic vars or universal bound vars in theorem?***From:*Gottfried Barrow

**Re: [isabelle] Schematic vars or universal bound vars in theorem?***From:*John Wickerson

- Previous by Date: Re: [isabelle] Locale interpretation introduces abbreviations rather than definitions
- Next by Date: [isabelle] General nitpick/sledge info & counterX found on 1 axiom 1 theorem
- Previous by Thread: Re: [isabelle] Schematic vars or universal bound vars in theorem?
- Next by Thread: Re: [isabelle] Schematic vars or universal bound vars in theorem?
- Cl-isabelle-users July 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