src/HOL/ex/ApproximationEx.thy
changeset 30413 c41afa5607be
parent 30122 1c912a9d8200
     1.1 --- a/src/HOL/ex/ApproximationEx.thy	Tue Mar 10 11:01:28 2009 +0100
     1.2 +++ b/src/HOL/ex/ApproximationEx.thy	Tue Mar 10 16:36:22 2009 +0100
     1.3 @@ -3,7 +3,7 @@
     1.4  *)
     1.5  
     1.6  theory ApproximationEx
     1.7 -imports "~~/src/HOL/Reflection/Approximation"
     1.8 +imports "~~/src/HOL/Decision_Procs/Approximation"
     1.9  begin
    1.10  
    1.11  text {*
    1.12 @@ -39,9 +39,14 @@
    1.13  lemma "0.5 \<le> x \<and> x \<le> 4.5 \<Longrightarrow> \<bar> arctan x - 0.91 \<bar> < 0.455"
    1.14    by (approximation 10)
    1.15  
    1.16 +lemma "0.49 \<le> x \<and> x \<le> 4.49 \<Longrightarrow> \<bar> arctan x - 0.91 \<bar> < 0.455"
    1.17 +  by (approximation 20)
    1.18 +
    1.19 +lemma "1 * pow2 -1 \<le> x \<and> x \<le> 9 * pow2 -1 \<Longrightarrow> \<bar> arctan x - 0.91 \<bar> < 0.455"
    1.20 +  by (approximation 10)
    1.21 +
    1.22  lemma "0 \<le> x \<and> x \<le> 1 \<Longrightarrow> 0 \<le> sin x"
    1.23    by (approximation 10)
    1.24  
    1.25 -
    1.26  end
    1.27