# HG changeset patch
# User huffman
# Date 1266957332 28800
# Node ID 8e1f994c6e54cb447d7c5b0e4928c3768d3d782c
# Parent  04d01ad972672f0a3547e19d6e2d34fed629fcef
adapt to new realpow rules

diff -r 04d01ad97267 -r 8e1f994c6e54 src/HOL/Decision_Procs/Approximation.thy
--- a/src/HOL/Decision_Procs/Approximation.thy	Tue Feb 23 11:14:09 2010 -0800
+++ b/src/HOL/Decision_Procs/Approximation.thy	Tue Feb 23 12:35:32 2010 -0800
@@ -1541,7 +1541,7 @@
     hence "real ?num \<noteq> 0" by auto
     have e_nat: "int (nat e) = e" using `0 \<le> e` by auto
     have num_eq: "real ?num = real (- floor_fl x)" using `0 < nat (- m)`
-      unfolding Float_floor real_of_float_minus real_of_float_simp real_of_nat_mult pow2_int[of "nat e", unfolded e_nat] realpow_real_of_nat[symmetric] by auto
+      unfolding Float_floor real_of_float_minus real_of_float_simp real_of_nat_mult pow2_int[of "nat e", unfolded e_nat] real_of_nat_power by auto
     have "0 < - floor_fl x" using `0 < ?num`[unfolded real_of_nat_less_iff[symmetric]] unfolding less_float_def num_eq[symmetric] real_of_float_0 real_of_nat_zero .
     hence "real (floor_fl x) < 0" unfolding less_float_def by auto