src/HOL/Algebra/Sylow.thy
changeset 68399 0b71d08528f0
parent 67613 ce654b0e6d69
child 68443 43055b016688
     1.1 --- a/src/HOL/Algebra/Sylow.thy	Tue Jun 05 16:35:52 2018 +0200
     1.2 +++ b/src/HOL/Algebra/Sylow.thy	Wed Jun 06 14:25:53 2018 +0100
     1.3 @@ -79,7 +79,7 @@
     1.4    show ?thesis
     1.5    proof
     1.6      show "inj_on (\<lambda>z\<in>H. m1 \<otimes> z) H"
     1.7 -      by (simp add: inj_on_def l_cancel [of m1 x y, THEN iffD1] H_def m1)
     1.8 +      by (simp add: H_def inj_on_def m1)
     1.9      show "restrict ((\<otimes>) m1) H \<in> H \<rightarrow> M1"
    1.10      proof (rule restrictI)
    1.11        fix z