# HG changeset patch
# User nipkow
# Date 1251482538 -7200
# Node ID 0273a2f787eac8c55adc74594bcd4fb591521d37
# Parent  153965be0f4b94e3a53b0d2c67c568aaab28cef7
tuned proofs

diff -r 153965be0f4b -r 0273a2f787ea src/HOL/Decision_Procs/Approximation.thy
--- a/src/HOL/Decision_Procs/Approximation.thy	Fri Aug 28 19:49:05 2009 +0200
+++ b/src/HOL/Decision_Procs/Approximation.thy	Fri Aug 28 20:02:18 2009 +0200
@@ -1904,7 +1904,7 @@
 	show "0 < real x * 2/3" using * by auto
 	show "real ?max + 1 \<le> real x * 2/3" using * up
 	  by (cases "0 < real x * real (lapprox_posrat prec 2 3) - 1",
-	      auto simp add: real_of_float_max max_def)
+	      auto simp add: real_of_float_max)
       qed
       finally have "real (?lb_horner (Float 1 -1)) + real (?lb_horner ?max)
 	\<le> ln (real x)"
diff -r 153965be0f4b -r 0273a2f787ea src/HOL/Decision_Procs/Ferrack.thy
--- a/src/HOL/Decision_Procs/Ferrack.thy	Fri Aug 28 19:49:05 2009 +0200
+++ b/src/HOL/Decision_Procs/Ferrack.thy	Fri Aug 28 20:02:18 2009 +0200
@@ -512,7 +512,7 @@
   assumes g0: "numgcd t = 0"
   shows "Inum bs t = 0"
   using g0[simplified numgcd_def] 
-  by (induct t rule: numgcdh.induct, auto simp add: natabs0 max_def maxcoeff_pos)
+  by (induct t rule: numgcdh.induct, auto simp add: natabs0 maxcoeff_pos)
 
 lemma numgcdh_pos: assumes gp: "g \<ge> 0" shows "numgcdh t g \<ge> 0"
   using gp