src/HOL/Equiv_Relations.thy
changeset 17589 58eeffd73be1
parent 15539 333a88244569
child 18490 434e34392c40
     1.1 --- a/src/HOL/Equiv_Relations.thy	Thu Sep 22 23:55:42 2005 +0200
     1.2 +++ b/src/HOL/Equiv_Relations.thy	Thu Sep 22 23:56:15 2005 +0200
     1.3 @@ -35,7 +35,7 @@
     1.4    apply (unfold equiv_def)
     1.5    apply clarify
     1.6    apply (rule equalityI)
     1.7 -   apply (rules intro: sym_trans_comp_subset refl_comp_subset)+
     1.8 +   apply (iprover intro: sym_trans_comp_subset refl_comp_subset)+
     1.9    done
    1.10  
    1.11  text {* Second half. *}
    1.12 @@ -73,7 +73,7 @@
    1.13  
    1.14  lemma eq_equiv_class:
    1.15      "r``{a} = r``{b} ==> equiv A r ==> b \<in> A ==> (a, b) \<in> r"
    1.16 -  by (rules intro: equalityD2 subset_equiv_class)
    1.17 +  by (iprover intro: equalityD2 subset_equiv_class)
    1.18  
    1.19  lemma equiv_class_nondisjoint:
    1.20      "equiv A r ==> x \<in> (r``{a} \<inter> r``{b}) ==> (a, b) \<in> r"