--- a/src/HOL/Equiv_Relations.thy Thu Sep 22 23:55:42 2005 +0200
+++ b/src/HOL/Equiv_Relations.thy Thu Sep 22 23:56:15 2005 +0200
@@ -35,7 +35,7 @@
apply (unfold equiv_def)
apply clarify
apply (rule equalityI)
- apply (rules intro: sym_trans_comp_subset refl_comp_subset)+
+ apply (iprover intro: sym_trans_comp_subset refl_comp_subset)+
done
text {* Second half. *}
@@ -73,7 +73,7 @@
lemma eq_equiv_class:
"r``{a} = r``{b} ==> equiv A r ==> b \<in> A ==> (a, b) \<in> r"
- by (rules intro: equalityD2 subset_equiv_class)
+ by (iprover intro: equalityD2 subset_equiv_class)
lemma equiv_class_nondisjoint:
"equiv A r ==> x \<in> (r``{a} \<inter> r``{b}) ==> (a, b) \<in> r"