--- 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)"
--- 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