src/HOL/Int.thy
 changeset 57512 cc97b347b301 parent 56889 48a745e1bde7 child 57514 bdc2c6b40bf2
```     1.1 --- a/src/HOL/Int.thy	Fri Jul 04 20:07:08 2014 +0200
1.2 +++ b/src/HOL/Int.thy	Fri Jul 04 20:18:47 2014 +0200
1.3 @@ -567,7 +567,7 @@
1.4    "(1 + z + z < 0) = (z < (0::int))"
1.5  proof (cases z)
1.6    case (nonneg n)
1.9                               le_imp_0_less [THEN order_less_imp_le])
1.10  next
1.11    case (neg n)
1.12 @@ -585,7 +585,7 @@
1.13    case (nonneg n)
1.15    thus ?thesis using  le_imp_0_less [OF le]
1.18  next
1.19    case (neg n)
1.20    show ?thesis
1.21 @@ -594,7 +594,7 @@
1.22      have "(0::int) < 1 + (int n + int n)"
1.24      also have "... = - (1 + z + z)"
1.27      also have "... = 0" by (simp add: eq)
1.28      finally have "0<0" ..
1.29      thus False by blast
1.30 @@ -1079,7 +1079,7 @@
1.31  lemma zmult_eq_1_iff: "(m*n = (1::int)) = ((m = 1 & n = 1) | (m = -1 & n = -1))"
1.32  apply (rule iffI)
1.33   apply (frule pos_zmult_eq_1_iff_lemma)
1.34 - apply (simp add: mult_commute [of m])
1.35 + apply (simp add: mult.commute [of m])
1.36   apply (frule pos_zmult_eq_1_iff_lemma, auto)
1.37  done
1.38
1.39 @@ -1238,7 +1238,7 @@
1.40  lemma zdvd_antisym_nonneg:
1.41      "0 <= m ==> 0 <= n ==> m dvd n ==> n dvd m ==> m = (n::int)"
1.42    apply (simp add: dvd_def, auto)
1.43 -  apply (auto simp add: mult_assoc zero_le_mult_iff zmult_eq_1_iff)
1.44 +  apply (auto simp add: mult.assoc zero_le_mult_iff zmult_eq_1_iff)
1.45    done
1.46
1.47  lemma zdvd_antisym_abs: assumes "(a::int) dvd b" and "b dvd a"
1.48 @@ -1251,7 +1251,7 @@
1.49    from `b dvd a` obtain k' where k':"a = b*k'" unfolding dvd_def by blast
1.50    from k k' have "a = a*k*k'" by simp
1.51    with mult_cancel_left1[where c="a" and b="k*k'"]
1.52 -  have kk':"k*k' = 1" using `a\<noteq>0` by (simp add: mult_assoc)
1.53 +  have kk':"k*k' = 1" using `a\<noteq>0` by (simp add: mult.assoc)
1.54    hence "k = 1 \<and> k' = 1 \<or> k = -1 \<and> k' = -1" by (simp add: zmult_eq_1_iff)
1.55    thus ?thesis using k k' by auto
1.56  qed
1.57 @@ -1301,7 +1301,7 @@
1.58  proof-
1.59    from d obtain h where h: "k*n = k*m * h" unfolding dvd_def by blast
1.60    {assume "n \<noteq> m*h" hence "k* n \<noteq> k* (m*h)" using kz by simp
1.61 -    with h have False by (simp add: mult_assoc)}
1.62 +    with h have False by (simp add: mult.assoc)}
1.63    hence "n = m * h" by blast
1.64    thus ?thesis by simp
1.65  qed
```