*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*: Mon, 23 Jul 2012 10:45:40 -0500*In-reply-to*: <AD8A5F2D-4D77-49E9-B9E8-B14C322D4ACA@cam.ac.uk>*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> <500B9DC5.4050703@gmx.com> <500BB792.9020401@jaist.ac.jp> <500C22E9.3070108@gmx.com> <500CBACC.9000805@jaist.ac.jp> <AD8A5F2D-4D77-49E9-B9E8-B14C322D4ACA@cam.ac.uk>*User-agent*: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:11.0) Gecko/20120312 Thunderbird/11.0

On 7/23/2012 3:03 AM, Lawrence Paulson wrote:

Personally, I think there is nothing wrong with asserting some axioms as the foundation of a brand-new development. If they are inconsistent, your work is worthless, but if they are the sole basis of your work, putting them in a locale wouldn't change things even a little bit. If you already have a sound and working development, that's a different situation altogether. Then it would make sense to encapsulate the axioms.

Regards, GB

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

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

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

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

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

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

- Previous by Date: Re: [isabelle] Isabelle/jedit
- 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