| changeset 63417 | c184ec919c70 |
| parent 63367 | 6c731c8b7f03 |
| child 63467 | f3781c5fb03f |
--- a/src/HOL/Transcendental.thy Fri Jul 08 23:43:11 2016 +0200 +++ b/src/HOL/Transcendental.thy Sat Jul 09 13:26:16 2016 +0200 @@ -36,7 +36,7 @@ by (metis of_nat_fact of_real_of_nat_eq) lemma pochhammer_of_real: "pochhammer (of_real x) n = of_real (pochhammer x n)" - by (simp add: pochhammer_def) + by (simp add: pochhammer_setprod) lemma norm_fact [simp]: "norm (fact n :: 'a :: {real_normed_algebra_1}) = fact n"