src/HOL/Decision_Procs/ex/Approximation_Quickcheck_Ex.thy
changeset 60017 b785d6d06430
parent 58988 6ebf918128b9
child 61586 5197a2ecb658
     1.1 --- a/src/HOL/Decision_Procs/ex/Approximation_Quickcheck_Ex.thy	Thu Apr 09 20:42:38 2015 +0200
     1.2 +++ b/src/HOL/Decision_Procs/ex/Approximation_Quickcheck_Ex.thy	Sat Apr 11 11:56:40 2015 +0100
     1.3 @@ -28,7 +28,7 @@
     1.4  
     1.5  lemma
     1.6    fixes x::real
     1.7 -  shows "x > 1 \<Longrightarrow> x \<le> 2 powr 20 * log 2 x + 1 \<and> (sin x)\<^sup>2 + (cos x)\<^sup>2 = 1"
     1.8 +  shows "x > 1 \<Longrightarrow> x \<le> 2 ^ 20 * log 2 x + 1 \<and> (sin x)\<^sup>2 + (cos x)\<^sup>2 = 1"
     1.9    using [[quickcheck_approximation_custom_seed = 1]]
    1.10    using [[quickcheck_approximation_epsilon = 0.00000001]]
    1.11      --\<open>avoids spurious counterexamples in approximate computation of @{term "(sin x)\<^sup>2 + (cos x)\<^sup>2"}