*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 11:14:01 -0500*In-reply-to*: <500C22E9.3070108@gmx.com>*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>*User-agent*: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:11.0) Gecko/20120312 Thunderbird/11.0

On 7/22/2012 10:57 AM, Gottfried Barrow wrote:

To make a long story short, if I give Sledgehammer a theorem that's only HOL, and HOL is consistent, then Sledgehammer can only prove that the theorem is true or that its negation is false.

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

- Previous by Date: Re: [isabelle] Schematic vars or universal bound vars in theorem?
- Next by Date: Re: [isabelle] Changing the arity of a term in ML
- 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