*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*: Sun, 22 Jul 2012 01:29:25 -0500*In-reply-to*: <alpine.LNX.2.00.1207212030180.15809@macbroy21.informatik.tu-muenchen.de>*References*: <5006C3EC.50004@gmx.com> <485EE543-83A4-4296-A6EB-2FCC934E3825@cam.ac.uk> <5006F2E1.3090605@gmx.com> <alpine.LNX.2.00.1207212030180.15809@macbroy21.informatik.tu-muenchen.de>*User-agent*: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:11.0) Gecko/20120312 Thunderbird/11.0

On 7/21/2012 1:32 PM, Makarius wrote:

On Wed, 18 Jul 2012, Gottfried Barrow wrote:It's my healthy paranoia kicking in here. I'm using axioms, so I'm trying to use everything I know right now to keep from being inconsistent.The best way is not to use axioms then. In mathematics you define new things by using old ones, and then prove the desired properties. Sometimes you work with abstract theories, but that corresponds to a locale or class definition in Isabelle/HOL, not axiomatization.

Giving opinions. That's the easy part. Regards, GB

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

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

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

- Previous by Date: Re: [isabelle] [Q]Question about Isabelle/hol
- Next by Date: Re: [isabelle] Schematic vars or universal bound vars in 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