Re: [isabelle] Introduction rule for quantifiers over sets of pairs



Using allI twice (or with +) does not work for me, but clarify does the job perfectly. Thanks a lot!

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







This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.