src/HOL/Multivariate_Analysis/ex/Approximations.thy
changeset 63417 c184ec919c70
parent 63040 eb4ddd18d635
     1.1 --- a/src/HOL/Multivariate_Analysis/ex/Approximations.thy	Fri Jul 08 23:43:11 2016 +0200
     1.2 +++ b/src/HOL/Multivariate_Analysis/ex/Approximations.thy	Sat Jul 09 13:26:16 2016 +0200
     1.3 @@ -185,11 +185,11 @@
     1.4    also have "\<dots> = (\<Sum>k\<le>n. 1 / fact k)"
     1.5    proof (intro setsum.cong refl)
     1.6      fix k assume k: "k \<in> {..n}"
     1.7 -    have "fact n = (\<Prod>i=1..n. real i)" by (rule fact_altdef)
     1.8 +    have "fact n = (\<Prod>i=1..n. real i)" by (simp add: fact_setprod)
     1.9      also from k have "{1..n} = {1..k} \<union> {k+1..n}" by auto
    1.10      also have "setprod real \<dots> / (\<Prod>i=k+1..n. real i) = (\<Prod>i=1..k. real i)"
    1.11        by (subst nonzero_divide_eq_eq, simp, subst setprod.union_disjoint [symmetric]) auto
    1.12 -    also have "\<dots> = fact k" by (simp only: fact_altdef)
    1.13 +    also have "\<dots> = fact k" by (simp add: fact_setprod)
    1.14      finally show "1 / (fact n / setprod real {k + 1..n}) = 1 / fact k" by simp
    1.15    qed
    1.16    also have "\<dots> = euler_approx n" by (simp add: euler_approx_def field_simps)