*To*: David Cock <david.cock at inf.ethz.ch>*Subject*: Re: [isabelle] universal quantifiers vs. schematic variables*From*: Jasmin Blanchette <jasmin.blanchette at inria.fr>*Date*: Sun, 4 Oct 2015 20:19:20 +0200*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <561169D0.1020100@inf.ethz.ch>*References*: <CAGOKs08m2EpBhQcrCb5n6t0VqtpesC2T1iia32d9rA0oCfhtcQ@mail.gmail.com> <561169D0.1020100@inf.ethz.ch>

David, > you've just discovered one of Isabelle's most fundamental quirks. As theorems, you're right that they're (logically) equivalent, but they differ if they appear as assumptions i.e. > > (!x. P x) => P y > > holds, but > > P ?x => P y > > does not (necessarily) hold. Huh? schematic_lemma "P ?x ==> P y" by assumption Cheers, Jasmin

**Follow-Ups**:**Re: [isabelle] universal quantifiers vs. schematic variables***From:*David Cock

**References**:**[isabelle] universal quantifiers vs. schematic variables***From:*noam neer

**Re: [isabelle] universal quantifiers vs. schematic variables***From:*David Cock

- Previous by Date: Re: [isabelle] universal quantifiers vs. schematic variables
- Next by Date: Re: [isabelle] universal quantifiers vs. schematic variables
- Previous by Thread: Re: [isabelle] universal quantifiers vs. schematic variables
- Next by Thread: Re: [isabelle] universal quantifiers vs. schematic variables
- Cl-isabelle-users October 2015 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