1.1 --- a/src/HOL/Decision_Procs/Approximation.thy	Fri Aug 19 17:05:10 2011 +0900
     1.2 +++ b/src/HOL/Decision_Procs/Approximation.thy	Fri Aug 19 07:45:22 2011 -0700
     1.3 @@ -959,7 +959,7 @@
     1.4      hence "0 \<le> cos t" using `0 < t` and cos_ge_zero by auto
     1.5      ultimately have even: "even n \<Longrightarrow> 0 \<le> ?rest" and odd: "odd n \<Longrightarrow> 0 \<le> - ?rest " by auto
     1.6  
     1.7 -    have "0 < ?fact" by (rule real_of_nat_fact_gt_zero)
     1.8 +    have "0 < ?fact" by (simp del: fact_Suc)
     1.9      have "0 < ?pow" using `0 < real x` by (rule zero_less_power)
    1.10  
    1.11      {