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

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.


On Nov 16, 2012, at 10:14 AM, Stephan van Staden <Stephan.vanStaden at> 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.