src/HOL/Decision_Procs/ex/Approximation_Ex.thy
changeset 60017 b785d6d06430
parent 59658 0cc388370041
child 60533 1e7ccd864b62
     1.1 --- a/src/HOL/Decision_Procs/ex/Approximation_Ex.thy	Thu Apr 09 20:42:38 2015 +0200
     1.2 +++ b/src/HOL/Decision_Procs/ex/Approximation_Ex.thy	Sat Apr 11 11:56:40 2015 +0100
     1.3 @@ -35,7 +35,7 @@
     1.4  
     1.5  section "Compute some transcendental values"
     1.6  
     1.7 -lemma "\<bar> ln 2 - 544531980202654583340825686620847 / 785593587443817081832229725798400 \<bar> < inverse (2^51) "
     1.8 +lemma "\<bar> ln 2 - 544531980202654583340825686620847 / 785593587443817081832229725798400 \<bar> < (inverse (2^51) :: real)"
     1.9    by (approximation 60)
    1.10  
    1.11  lemma "\<bar> exp 1.626 - 5.083499996273 \<bar> < (inverse 10 ^ 10 :: real)"