Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/ex/ApproximationEx.thy
changeset 30413 c41afa5607be
parent 30122 1c912a9d8200 
--- a/src/HOL/ex/ApproximationEx.thy	Tue Mar 10 11:01:28 2009 +0100
+++ b/src/HOL/ex/ApproximationEx.thy	Tue Mar 10 16:36:22 2009 +0100
@@ -3,7 +3,7 @@
 *)
 
 theory ApproximationEx
-imports "~~/src/HOL/Reflection/Approximation"
+imports "~~/src/HOL/Decision_Procs/Approximation"
 begin
 
 text {*
@@ -39,9 +39,14 @@
 lemma "0.5 \<le> x \<and> x \<le> 4.5 \<Longrightarrow> \<bar> arctan x - 0.91 \<bar> < 0.455"
   by (approximation 10)
 
+lemma "0.49 \<le> x \<and> x \<le> 4.49 \<Longrightarrow> \<bar> arctan x - 0.91 \<bar> < 0.455"
+  by (approximation 20)
+
+lemma "1 * pow2 -1 \<le> x \<and> x \<le> 9 * pow2 -1 \<Longrightarrow> \<bar> arctan x - 0.91 \<bar> < 0.455"
+  by (approximation 10)
+
 lemma "0 \<le> x \<and> x \<le> 1 \<Longrightarrow> 0 \<le> sin x"
   by (approximation 10)
 
-
 end
isabelle