src/HOL/Rat.thy
changeset 64240 eabf80376aab
parent 63911 d00d4f399f05
child 64267 b9a1486e79be
     1.1 --- a/src/HOL/Rat.thy	Sun Oct 16 09:31:03 2016 +0200
     1.2 +++ b/src/HOL/Rat.thy	Sun Oct 16 09:31:04 2016 +0200
     1.3 @@ -295,10 +295,10 @@
     1.4          (q * gcd r s) * (sgn (q * s) * r * gcd p q)"
     1.5        by simp
     1.6      with assms show ?thesis
     1.7 -      by (auto simp add: ac_simps sgn_times sgn_0_0)
     1.8 +      by (auto simp add: ac_simps sgn_mult sgn_0_0)
     1.9    qed
    1.10    from assms show ?thesis
    1.11 -    by (auto simp: normalize_def Let_def dvd_div_div_eq_mult mult.commute sgn_times
    1.12 +    by (auto simp: normalize_def Let_def dvd_div_div_eq_mult mult.commute sgn_mult
    1.13          split: if_splits intro: *)
    1.14  qed
    1.15  
    1.16 @@ -651,7 +651,7 @@
    1.17        @{thm True_implies_equals},
    1.18        @{thm distrib_left [where a = "numeral v" for v]},
    1.19        @{thm distrib_left [where a = "- numeral v" for v]},
    1.20 -      @{thm divide_1}, @{thm divide_zero_left},
    1.21 +      @{thm div_by_1}, @{thm div_0},
    1.22        @{thm times_divide_eq_right}, @{thm times_divide_eq_left},
    1.23        @{thm minus_divide_left} RS sym, @{thm minus_divide_right} RS sym,
    1.24        @{thm add_divide_distrib}, @{thm diff_divide_distrib},