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)
```