--- a/src/HOL/Decision_Procs/ex/Approximation_Ex.thy Wed Mar 11 12:51:00 2009 +0100
+++ b/src/HOL/Decision_Procs/ex/Approximation_Ex.thy Wed Mar 11 13:53:51 2009 +0100
@@ -1,6 +1,4 @@
-(* Title: HOL/ex/ApproximationEx.thy
- Author: Johannes Hoelzl <hoelzl@in.tum.de> 2009
-*)
+(* Author: Johannes Hoelzl <hoelzl@in.tum.de> 2009 *)
theory Approximation_Ex
imports Complex_Main "~~/src/HOL/Decision_Procs/Approximation"
@@ -42,7 +40,7 @@
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"
+lemma "1 / 2^1 \<le> x \<and> x \<le> 9 / 2^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"