src/HOL/Algebra/IntRing.thy
changeset 57512 cc97b347b301
parent 55991 3fa6e6c81788
child 57514 bdc2c6b40bf2
     1.1 --- a/src/HOL/Algebra/IntRing.thy	Fri Jul 04 20:07:08 2014 +0200
     1.2 +++ b/src/HOL/Algebra/IntRing.thy	Fri Jul 04 20:18:47 2014 +0200
     1.3 @@ -271,11 +271,11 @@
     1.4    then have "p dvd a \<or> p dvd b"
     1.5      by (metis prime prime_dvd_mult_eq_int)
     1.6    then show "(\<exists>x. a = x * int p) \<or> (\<exists>x. b = x * int p)"
     1.7 -    by (metis dvd_def mult_commute)
     1.8 +    by (metis dvd_def mult.commute)
     1.9  next
    1.10    assume "UNIV = {uu. EX x. uu = x * int p}"
    1.11    then obtain x where "1 = x * int p" by best
    1.12 -  then have "\<bar>int p * x\<bar> = 1" by (simp add: mult_commute)
    1.13 +  then have "\<bar>int p * x\<bar> = 1" by (simp add: mult.commute)
    1.14    then show False
    1.15      by (metis abs_of_nat int_1 of_nat_eq_iff abs_zmult_eq_1 one_not_prime_nat prime)
    1.16  qed