src/HOL/Old_Number_Theory/Int2.thy

 proof -
   from `0 < z` have modth: "x mod z \<ge> 0" by simp
   have "(x div z) * z \<le> (x div z) * z" by simp
   then have "(x div z) * z \<le> (x div z) * z + x mod z" using modth by arith 
   also have "\<dots> = x"
-    by (auto simp add: zmod_zdiv_equality [symmetric] zmult_ac)
+    by (auto simp add: zmod_zdiv_equality [symmetric] mult_ac)
   also note `x < y * z`
   finally show ?thesis
     apply (auto simp add: mult_less_cancel_right)
     using assms apply arith
     done

   apply (auto simp add: int_distrib)
   done
 
 lemma zcong_zmult_prop2: "[a = b](mod m) ==>
     ([c = d * a](mod m) = [c = d * b] (mod m))"
-  by (auto simp add: zmult_ac zcong_zmult_prop1)
+  by (auto simp add: mult_ac zcong_zmult_prop1)
 
 lemma zcong_zmult_prop3: "[| zprime p; ~[x = 0] (mod p);
     ~[y = 0] (mod p) |] ==> ~[x * y = 0] (mod p)"
   apply (auto simp add: zcong_def)
   apply (drule zprime_zdvd_zmult_better, auto)
   done
 
 lemma zcong_less_eq: "[| 0 < x; 0 < y; 0 < m; [x = y] (mod m);
     x < m; y < m |] ==> x = y"
-  by (metis zcong_not zcong_sym zless_linear)
+  by (metis zcong_not zcong_sym less_linear)
 
 lemma zcong_neg_1_impl_ne_1:
   assumes "2 < p" and "[x = -1] (mod p)"
   shows "~([x = 1] (mod p))"
 proof

   finally (zcong_trans) show "[x * x ^ nat (p - 2) = 1] (mod p)" .
 qed
 
 lemma MultInv_prop2a: "[| 2 < p; zprime p; ~([x = 0](mod p)) |] ==>
     [(MultInv p x) * x = 1] (mod p)"
-  by (auto simp add: MultInv_prop2 zmult_ac)
+  by (auto simp add: MultInv_prop2 mult_ac)
 
 lemma aux_1: "2 < p ==> ((nat p) - 2) = (nat (p - 2))"
   by (simp add: nat_diff_distrib)
 
 lemma aux_2: "2 < p ==> 0 < nat (p - 2)"

     [(x * (MultInv p x) * (MultInv p (MultInv p x))) = x] (mod p)"
   apply (frule MultInv_prop3, auto)
   apply (insert MultInv_prop2 [of p "MultInv p x"], auto)
   apply (drule MultInv_prop2, auto)
   apply (drule_tac k = x in zcong_scalar2, auto)
-  apply (auto simp add: zmult_ac)
+  apply (auto simp add: mult_ac)
   done
 
 lemma MultInv_prop4: "[| 2 < p; zprime p; ~([x = 0](mod p)) |] ==>
     [(MultInv p (MultInv p x)) = x] (mod p)"
   apply (frule aux__1, auto)

     [x = y] (mod p)"
   apply (drule_tac a = "MultInv p x" and b = "MultInv p y" and
     m = p and k = x in zcong_scalar)
   apply (insert MultInv_prop2 [of p x], simp)
   apply (auto simp only: zcong_sym [of "MultInv p x * x"])
-  apply (auto simp add:  zmult_ac)
+  apply (auto simp add: mult_ac)
   apply (drule zcong_trans, auto)
   apply (drule_tac a = "x * MultInv p y" and k = y in zcong_scalar, auto)
-  apply (insert MultInv_prop2a [of p y], auto simp add: zmult_ac)
+  apply (insert MultInv_prop2a [of p y], auto simp add: mult_ac)
   apply (insert zcong_zmult_prop2 [of "y * MultInv p y" 1 p y x])
   apply (auto simp add: zcong_sym)
   done
 
 lemma MultInv_zcong_prop1: "[| 2 < p; [j = k] (mod p) |] ==>

 
 lemma aux___2: "[|2 < p; zprime p; ~([k = 0](mod p));
     [j * k = a * MultInv p k * k] (mod p) |] ==> [j * k = a] (mod p)"
   apply (insert MultInv_prop2a [of p k] zcong_zmult_prop2
     [of "MultInv p k * k" 1 p "j * k" a])
-  apply (auto simp add: zmult_ac)
+  apply (auto simp add: mult_ac)
   done
 
 lemma aux___3: "[j * k = a] (mod p) ==> [(MultInv p j) * j * k =
      (MultInv p j) * a] (mod p)"
-  by (auto simp add: zmult_assoc zcong_scalar2)
+  by (auto simp add: mult_assoc zcong_scalar2)
 
 lemma aux___4: "[|2 < p; zprime p; ~([j = 0](mod p));
     [(MultInv p j) * j * k = (MultInv p j) * a] (mod p) |]
        ==> [k = a * (MultInv p j)] (mod p)"
   apply (insert MultInv_prop2a [of p j] zcong_zmult_prop1
     [of "MultInv p j * j" 1 p "MultInv p j * a" k])
-  apply (auto simp add: zmult_ac zcong_sym)
+  apply (auto simp add: mult_ac zcong_sym)
   done
 
 lemma MultInv_zcong_prop2: "[| 2 < p; zprime p; ~([k = 0](mod p));
     ~([j = 0](mod p)); [j = a * MultInv p k] (mod p) |] ==>
     [k = a * MultInv p j] (mod p)"