*To*: Stephan Merz <Stephan.Merz at loria.fr>*Subject*: Re: [isabelle] Introduction rule for quantifiers over sets of pairs*From*: Stephan van Staden <Stephan.vanStaden at inf.ethz.ch>*Date*: Fri, 16 Nov 2012 14:34:59 +0100*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <C826BDFF-0492-4A47-9C97-AAE2F1E07E76@loria.fr>*References*: <50A63C1B.6010501@inf.ethz.ch> <C826BDFF-0492-4A47-9C97-AAE2F1E07E76@loria.fr>*User-agent*: Mozilla/5.0 (X11; Linux i686; rv:16.0) Gecko/20121028 Thunderbird/16.0.2

Stephan On 11/16/2012 02:23 PM, Stephan Merz wrote:

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**:

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

**Re: [isabelle] Introduction rule for quantifiers over sets of pairs***From:*Stephan Merz

- Previous by Date: Re: [isabelle] isabelle mailing lists
- Next by Date: Re: [isabelle] Isabelle-friendly CPUs and benchmarks
- Previous by Thread: Re: [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