*To*: Gottfried Barrow <gottfried.barrow at gmx.com>*Subject*: Re: [isabelle] Schematic vars or universal bound vars in theorem?*From*: Makarius <makarius at sketis.net>*Date*: Sat, 21 Jul 2012 20:32:56 +0200 (CEST)*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <5006F2E1.3090605@gmx.com>*References*: <5006C3EC.50004@gmx.com> <485EE543-83A4-4296-A6EB-2FCC934E3825@cam.ac.uk> <5006F2E1.3090605@gmx.com>*User-agent*: Alpine 2.00 (LNX 1167 2008-08-23)

On Wed, 18 Jul 2012, Gottfried Barrow wrote:

It's my healthy paranoia kicking in here. I'm using axioms, so I'mtrying to use everything I know right now to keep from beinginconsistent.

Makarius

**Follow-Ups**:**Re: [isabelle] Schematic vars or universal bound vars in theorem?***From:*Gottfried Barrow

**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

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

- Previous by Date: Re: [isabelle] Failing simproc
- Next by Date: Re: [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