src/HOL/Algebra/IntRing.thy
changeset 44821 a92f65e174cf
parent 44655 fe0365331566
child 49962 a8cc904a6820
     1.1 --- a/src/HOL/Algebra/IntRing.thy	Wed Sep 07 14:58:40 2011 +0200
     1.2 +++ b/src/HOL/Algebra/IntRing.thy	Wed Sep 07 09:02:58 2011 -0700
     1.3 @@ -35,8 +35,8 @@
     1.4    apply (rule abelian_groupI, simp_all)
     1.5    defer 1
     1.6    apply (rule comm_monoidI, simp_all)
     1.7 - apply (rule zadd_zmult_distrib)
     1.8 -apply (fast intro: zadd_zminus_inverse2)
     1.9 + apply (rule left_distrib)
    1.10 +apply (fast intro: left_minus)
    1.11  done
    1.12  
    1.13  (*
    1.14 @@ -298,7 +298,7 @@
    1.15    from this obtain x 
    1.16        where "1 = x * p" by best
    1.17    from this [symmetric]
    1.18 -      have "p * x = 1" by (subst zmult_commute)
    1.19 +      have "p * x = 1" by (subst mult_commute)
    1.20    hence "\<bar>p * x\<bar> = 1" by simp
    1.21    hence "\<bar>p\<bar> = 1" by (rule abs_zmult_eq_1)
    1.22    from this and prime