*To*: Stephan van Staden <Stephan.vanStaden at inf.ethz.ch>*Subject*: Re: [isabelle] Introduction rule for quantifiers over sets of pairs*From*: Stephan Merz <Stephan.Merz at loria.fr>*Date*: Fri, 16 Nov 2012 10:23:20 -0300*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <50A63C1B.6010501@inf.ethz.ch>*References*: <50A63C1B.6010501@inf.ethz.ch>

There is not a single rule that would introduce two quantifiers. You can either use rule allI twice (see the Isar combinator "+") or use the clarify method. Stephan On Nov 16, 2012, at 10:14 AM, Stephan van Staden <Stephan.vanStaden at inf.ethz.ch> wrote: > Dear all, > > This one should be simple. I'm looking for the name of the rule that will do the job of RRR below: > > lemma "\<forall> (a,b) \<in> S. P" > proof (rule RRR) > fix a b > assume "(a,b) \<in> S" > show "P" sorry > qed > > Thanks in advance! > > Stephan >

**Follow-Ups**:**Re: [isabelle] Introduction rule for quantifiers over sets of pairs***From:*Stephan van Staden

**References**:**[isabelle] Introduction rule for quantifiers over sets of pairs***From:*Stephan van Staden

- Previous by Date: [isabelle] Introduction rule for quantifiers over sets of pairs
- Next by Date: Re: [isabelle] isabelle mailing lists
- Previous by Thread: [isabelle] Introduction rule for quantifiers over sets of pairs
- Next by Thread: Re: [isabelle] Introduction rule for quantifiers over sets of pairs
- Cl-isabelle-users November 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