--- a/src/HOL/Decision_Procs/Approximation.thy Sat Mar 24 16:27:04 2012 +0100
+++ b/src/HOL/Decision_Procs/Approximation.thy Sun Mar 25 20:15:39 2012 +0200
@@ -1350,7 +1350,7 @@
also have "\<dots> \<le> cos ((?ux - 2 * ?lpi))"
using cos_monotone_minus_pi_0'[OF pi_x x_le_ux ux_0]
by (simp only: real_of_float_minus real_of_int_minus real_of_one
- number_of_Min diff_minus mult_minus_left mult_1_left)
+ minus_one [symmetric] diff_minus mult_minus_left mult_1_left)
also have "\<dots> = cos ((- (?ux - 2 * ?lpi)))"
unfolding real_of_float_minus cos_minus ..
also have "\<dots> \<le> (ub_cos prec (- (?ux - 2 * ?lpi)))"
@@ -1394,7 +1394,7 @@
also have "\<dots> \<le> cos ((?lx + 2 * ?lpi))"
using cos_monotone_0_pi'[OF lx_0 lx_le_x pi_x]
by (simp only: real_of_float_minus real_of_int_minus real_of_one
- number_of_Min diff_minus mult_minus_left mult_1_left)
+ minus_one [symmetric] diff_minus mult_minus_left mult_1_left)
also have "\<dots> \<le> (ub_cos prec (?lx + 2 * ?lpi))"
using lb_cos[OF lx_0 pi_lx] by simp
finally show ?thesis unfolding u by (simp add: real_of_float_max)
@@ -2117,7 +2117,8 @@
lemma interpret_floatarith_num:
shows "interpret_floatarith (Num (Float 0 0)) vs = 0"
and "interpret_floatarith (Num (Float 1 0)) vs = 1"
- and "interpret_floatarith (Num (Float (number_of a) 0)) vs = number_of a" by auto
+ and "interpret_floatarith (Num (Float (numeral a) 0)) vs = numeral a"
+ and "interpret_floatarith (Num (Float (neg_numeral a) 0)) vs = neg_numeral a" by auto
subsection "Implement approximation function"