*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Thanks Nitpick for actually answering a former, simple question*From*: Lars Noschinski <noschinl at in.tum.de>*Date*: Tue, 11 Sep 2012 22:52:30 +0200*In-reply-to*: <504F99E9.8060608@gmx.com>*References*: <504F99E9.8060608@gmx.com>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:10.0.6esrpre) Gecko/20120817 Icedove/10.0.6

On 11.09.2012 22:07, Gottfried Barrow wrote:

Hello, Like two months ago, I specifically asked, in a fairly precise way, "What's the difference between free variables and universally quantified variables, and is there a reason I shouldn't use free variables?"

[...] For a free variable a not bound in any enclosing context, 'lemma "P a"'

theorem "~((A --> B --> A) --> (A <-> B))"

"!a b. ~(P a b)"

theorem "(A --> B --> A) --> (A <-> B)"

"!a b. P a b"

theorem "~(!A. !B.(A --> B --> A) --> (A <-> B))"

"~(!a b. P a b)" -- Lars

**References**:**[isabelle] Thanks Nitpick for actually answering a former, simple question***From:*Gottfried Barrow

- Previous by Date: [isabelle] Thanks Nitpick for actually answering a former, simple question
- Next by Date: Re: [isabelle] Thanks Nitpick for actually answering a former, simple question
- Previous by Thread: [isabelle] Thanks Nitpick for actually answering a former, simple question
- Next by Thread: Re: [isabelle] Thanks Nitpick for actually answering a former, simple question
- Cl-isabelle-users September 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