[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
qed

Thanks in advance!

Stephan





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