src/HOL/Rat.thy

   proof -
     from that have "(p * gcd r s) * (sgn (q * s) * s * gcd p q) =
         (q * gcd r s) * (sgn (q * s) * r * gcd p q)"
       by simp
     with assms show ?thesis
-      by (auto simp add: ac_simps sgn_times sgn_0_0)
+      by (auto simp add: ac_simps sgn_mult sgn_0_0)
   qed
   from assms show ?thesis
-    by (auto simp: normalize_def Let_def dvd_div_div_eq_mult mult.commute sgn_times
+    by (auto simp: normalize_def Let_def dvd_div_div_eq_mult mult.commute sgn_mult
         split: if_splits intro: *)
 qed
 
 lemma normalize_eq: "normalize (a, b) = (p, q) \<Longrightarrow> Fract p q = Fract a b"
   by (auto simp: normalize_def Let_def Fract_coprime dvd_div_neg rat_number_collapse

     (* not needed because x < (y::int) can be rewritten as x + 1 <= y: of_int_less_iff RS iffD2 *)
   #> Lin_Arith.add_simps [@{thm neg_less_iff_less},
       @{thm True_implies_equals},
       @{thm distrib_left [where a = "numeral v" for v]},
       @{thm distrib_left [where a = "- numeral v" for v]},
-      @{thm divide_1}, @{thm divide_zero_left},
+      @{thm div_by_1}, @{thm div_0},
       @{thm times_divide_eq_right}, @{thm times_divide_eq_left},
       @{thm minus_divide_left} RS sym, @{thm minus_divide_right} RS sym,
       @{thm add_divide_distrib}, @{thm diff_divide_distrib},
       @{thm of_int_minus}, @{thm of_int_diff},
       @{thm of_int_of_nat_eq}]