src/HOL/Algebra/Coset.thy
changeset 40815 6e2d17cc0d1d
parent 39910 10097e0a9dbd
child 41528 276078f01ada
     1.1 --- a/src/HOL/Algebra/Coset.thy	Mon Nov 29 12:15:14 2010 +0100
     1.2 +++ b/src/HOL/Algebra/Coset.thy	Mon Nov 29 13:44:54 2010 +0100
     1.3 @@ -606,7 +606,7 @@
     1.4  proof -
     1.5    interpret group G by fact
     1.6    show ?thesis
     1.7 -  proof (intro equiv.intro)
     1.8 +  proof (intro equivI)
     1.9      show "refl_on (carrier G) (rcong H)"
    1.10        by (auto simp add: r_congruent_def refl_on_def) 
    1.11    next