src/HOL/Decision_Procs/Approximation.thy
 changeset 65578 e4997c181cce parent 65109 a79c1080f1e9 child 65582 a1bc1b020cf2
1.1 --- a/src/HOL/Decision_Procs/Approximation.thy	Tue Apr 25 08:38:23 2017 +0200
1.2 +++ b/src/HOL/Decision_Procs/Approximation.thy	Tue Apr 25 16:39:54 2017 +0100
1.3 @@ -1987,7 +1987,7 @@
1.4        have "exp x = exp (?num * (x / ?num))"
1.5          using \<open>real ?num \<noteq> 0\<close> by auto
1.6        also have "\<dots> = exp (x / ?num) ^ ?num"
1.7 -        unfolding exp_real_of_nat_mult ..
1.8 +        unfolding exp_of_nat_mult ..
1.9        also have "\<dots> \<le> exp (float_divr prec x (- floor_fl x)) ^ ?num"
1.10          unfolding num_eq fl_eq
1.11          by (rule power_mono, rule exp_le_cancel_iff[THEN iffD2], rule float_divr) auto
1.12 @@ -2023,7 +2023,7 @@
1.13            unfolding num_eq fl_eq
1.14            using float_divl by (auto intro!: power_mono simp del: uminus_float.rep_eq)
1.15          also have "\<dots> = exp (?num * (x / ?num))"
1.16 -          unfolding exp_real_of_nat_mult ..
1.17 +          unfolding exp_of_nat_mult ..
1.18          also have "\<dots> = exp x"
1.19            using \<open>real ?num \<noteq> 0\<close> by auto
1.20          finally show ?thesis
1.21 @@ -2050,7 +2050,7 @@
1.22          hence "real_of_float (Float 1 (- 2)) ^ ?num \<le> exp (x / (- floor_fl x)) ^ ?num"
1.23            by (metis Float_num(5) power_mono zero_le_divide_1_iff zero_le_numeral)
1.24          also have "\<dots> = exp x"
1.25 -          unfolding num_eq fl_eq exp_real_of_nat_mult[symmetric]
1.26 +          unfolding num_eq fl_eq exp_of_nat_mult[symmetric]
1.27            using \<open>real_of_float (floor_fl x) \<noteq> 0\<close> by auto
1.28          finally show ?thesis
1.29            unfolding lb_exp.simps if_not_P[OF \<open>\<not> 0 < x\<close>] if_P[OF \<open>x < - 1\<close>]