*To*: <cl-isabelle-users at lists.cam.ac.uk>*Subject*: [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:14:03 +0100*User-agent*: Mozilla/5.0 (X11; Linux i686; rv:16.0) Gecko/20121028 Thunderbird/16.0.2

Dear all,

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 Merz

**Re: [isabelle] Introduction rule for quantifiers over sets of pairs***From:*Tjark Weber

- Previous by Date: Re: [isabelle] Automatic derivation of a total order on datatypes
- Next by Date: Re: [isabelle] Introduction rule for quantifiers over sets of pairs
- Previous by Thread: [isabelle] New AFP entry: A Separation Logic Framework for Imperative HOL
- 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