src/HOL/PReal.thy
changeset 29667 53103fc8ffa3
parent 29197 6d4cb27ed19c
child 29811 026b0f9f579f
     1.1 --- a/src/HOL/PReal.thy	Sun Jan 18 13:58:17 2009 +0100
     1.2 +++ b/src/HOL/PReal.thy	Wed Jan 28 16:29:16 2009 +0100
     1.3 @@ -718,7 +718,7 @@
     1.4      case (Suc k)
     1.5        from this obtain b where "b \<in> A" "b + of_nat k * u \<in> A" ..
     1.6        hence "b + of_int (int k)*u + u \<in> A" by (simp add: prems)
     1.7 -      thus ?case by (force simp add: left_distrib add_ac prems) 
     1.8 +      thus ?case by (force simp add: algebra_simps prems) 
     1.9    qed
    1.10  next
    1.11    case (neg n)
    1.12 @@ -815,7 +815,7 @@
    1.13      proof -
    1.14        have "r + ?d < r + (r * ?d)/y" by (simp add: dless)
    1.15        also with ypos have "... = (r/y) * (y + ?d)"
    1.16 -	by (simp only: right_distrib divide_inverse mult_ac, simp)
    1.17 +	by (simp only: algebra_simps divide_inverse, simp)
    1.18        also have "... = r*x" using ypos
    1.19  	by (simp add: times_divide_eq_left) 
    1.20        finally show "r + ?d < r*x" .