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>]