[isabelle] Introduction rule for quantifiers over sets of pairs

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

Thanks in advance!


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