src/HOL/Decision_Procs/Approximation.thy
changeset 61649 268d88ec9087
parent 61610 4f54d2759a0b
child 61824 dcbe9f756ae0
     1.1 --- a/src/HOL/Decision_Procs/Approximation.thy	Thu Nov 12 11:22:26 2015 +0100
     1.2 +++ b/src/HOL/Decision_Procs/Approximation.thy	Fri Nov 13 12:27:13 2015 +0000
     1.3 @@ -808,7 +808,7 @@
     1.4          also note float_round_up
     1.5          finally have "pi / 2 - float_round_up prec (?ub_horner ?invx) \<le> arctan x"
     1.6            using \<open>0 \<le> arctan x\<close> arctan_inverse[OF \<open>1 / x \<noteq> 0\<close>]
     1.7 -          unfolding real_sgn_pos[OF \<open>0 < 1 / real_of_float x\<close>] le_diff_eq by auto
     1.8 +          unfolding sgn_pos[OF \<open>0 < 1 / real_of_float x\<close>] le_diff_eq by auto
     1.9          moreover
    1.10          have "lb_pi prec * Float 1 (- 1) \<le> pi / 2"
    1.11            unfolding Float_num times_divide_eq_right mult_1_left using pi_boundaries by simp
    1.12 @@ -935,7 +935,7 @@
    1.13          unfolding one_float.rep_eq[symmetric] by (rule arctan_monotone') (rule float_divl)
    1.14        finally have "arctan x \<le> pi / 2 - (?lb_horner ?invx)"
    1.15          using \<open>0 \<le> arctan x\<close> arctan_inverse[OF \<open>1 / x \<noteq> 0\<close>]
    1.16 -        unfolding real_sgn_pos[OF \<open>0 < 1 / x\<close>] le_diff_eq by auto
    1.17 +        unfolding sgn_pos[OF \<open>0 < 1 / x\<close>] le_diff_eq by auto
    1.18        moreover
    1.19        have "pi / 2 \<le> ub_pi prec * Float 1 (- 1)"
    1.20          unfolding Float_num times_divide_eq_right mult_1_right