src/HOL/Rat.thy
changeset 49962 a8cc904a6820
parent 48891 c0eafbd55de3
child 50178 ad52ddd35c3a
     1.1 --- a/src/HOL/Rat.thy	Fri Oct 19 10:46:42 2012 +0200
     1.2 +++ b/src/HOL/Rat.thy	Fri Oct 19 15:12:52 2012 +0200
     1.3 @@ -123,7 +123,7 @@
     1.4  
     1.5  lift_definition plus_rat :: "rat \<Rightarrow> rat \<Rightarrow> rat"
     1.6    is "\<lambda>x y. (fst x * snd y + fst y * snd x, snd x * snd y)"
     1.7 -  by (clarsimp, simp add: left_distrib, simp add: mult_ac)
     1.8 +  by (clarsimp, simp add: distrib_right, simp add: mult_ac)
     1.9  
    1.10  lemma add_rat [simp]:
    1.11    assumes "b \<noteq> 0" and "d \<noteq> 0"
    1.12 @@ -616,8 +616,8 @@
    1.13      (* not needed because x < (y::int) can be rewritten as x + 1 <= y: of_int_less_iff RS iffD2 *)
    1.14    #> Lin_Arith.add_simps [@{thm neg_less_iff_less},
    1.15        @{thm True_implies_equals},
    1.16 -      read_instantiate @{context} [(("a", 0), "(numeral ?v)")] @{thm right_distrib},
    1.17 -      read_instantiate @{context} [(("a", 0), "(neg_numeral ?v)")] @{thm right_distrib},
    1.18 +      read_instantiate @{context} [(("a", 0), "(numeral ?v)")] @{thm distrib_left},
    1.19 +      read_instantiate @{context} [(("a", 0), "(neg_numeral ?v)")] @{thm distrib_left},
    1.20        @{thm divide_1}, @{thm divide_zero_left},
    1.21        @{thm times_divide_eq_right}, @{thm times_divide_eq_left},
    1.22        @{thm minus_divide_left} RS sym, @{thm minus_divide_right} RS sym,