*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*: Wed, 18 Jul 2012 11:12:02 -0500*In-reply-to*: <5006C3EC.50004@gmx.com>*References*: <5006C3EC.50004@gmx.com>*User-agent*: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:11.0) Gecko/20120312 Thunderbird/11.0

This reply to my email is a basic logic fix, in case it matters to someone. For my equality axiom, I was using something like this: (1) "!u. !v. !x. ((x <\in> u <-> x <\in> v) --> u=v)", with a corresponding theorem like this: (2) "!u. !x. (~(x \<in> u) --> u = Sigma_E)". The textbook formula came to my mind, so I changed the axiom to: (3) "!u. !v. ((!x.(x \<in> u <-> x \<in> v)) --> u=v)".

(4) "!u. ((!x. ~(x \<in> u)) --> u = Sigma_E)". My questions about schematic vs. universal bound variables stay the same. Regards, GB

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

- Previous by Date: [isabelle] Schematic vars or universal bound vars in theorem?
- Next by Date: Re: [isabelle] Schematic vars or universal bound vars in theorem?
- Previous by Thread: [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