src/HOL/Real/RealDef.thy
changeset 23477 f4b83f03cac9
parent 23438 dd824e86fa8a
child 23482 2f4be6844f7c
     1.1 --- a/src/HOL/Real/RealDef.thy	Fri Jun 22 22:41:17 2007 +0200
     1.2 +++ b/src/HOL/Real/RealDef.thy	Sat Jun 23 19:33:22 2007 +0200
     1.3 @@ -253,8 +253,7 @@
     1.4  apply (rule_tac [2]
     1.5          x = "Abs_Real (realrel``{(inverse (D) + 1, 1)})" 
     1.6         in exI)
     1.7 -apply (auto simp add: real_mult ring_distrib
     1.8 -              preal_mult_inverse_right add_ac mult_ac)
     1.9 +apply (auto simp add: real_mult preal_mult_inverse_right ring_simps)
    1.10  done
    1.11  
    1.12  lemma real_mult_inverse_left: "x \<noteq> 0 ==> inverse(x)*x = (1::real)"
    1.13 @@ -632,7 +631,7 @@
    1.14    then have "real x / real d = ... / real d"
    1.15      by simp
    1.16    then show ?thesis
    1.17 -    by (auto simp add: add_divide_distrib ring_eq_simps prems)
    1.18 +    by (auto simp add: add_divide_distrib ring_simps prems)
    1.19  qed
    1.20  
    1.21  lemma real_of_int_div: "(d::int) ~= 0 ==> d dvd n ==>
    1.22 @@ -776,7 +775,7 @@
    1.23    then have "real x / real d = \<dots> / real d"
    1.24      by simp
    1.25    then show ?thesis
    1.26 -    by (auto simp add: add_divide_distrib ring_eq_simps prems)
    1.27 +    by (auto simp add: add_divide_distrib ring_simps prems)
    1.28  qed
    1.29  
    1.30  lemma real_of_nat_div: "0 < (d::nat) ==> d dvd n ==>