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.7 -  thus ?thesis by (simp add: linorder_not_less add_assoc add_increasing
     1.8 +  thus ?thesis by (simp add: linorder_not_less add.assoc add_increasing
     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.14    have le: "0 \<le> z+z" by (simp add: nonneg add_increasing) 
    1.15    thus ?thesis using  le_imp_0_less [OF le]
    1.16 -    by (auto simp add: add_assoc) 
    1.17 +    by (auto simp add: add.assoc) 
    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.23        by (simp add: le_imp_0_less add_increasing) 
    1.24      also have "... = - (1 + z + z)" 
    1.25 -      by (simp add: neg add_assoc [symmetric]) 
    1.26 +      by (simp add: neg add.assoc [symmetric]) 
    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