--- a/src/HOL/Library/Binomial.thy Fri Dec 06 23:36:28 2013 +0100
+++ b/src/HOL/Library/Binomial.thy Sat Dec 07 12:52:31 2013 +0100
@@ -184,8 +184,9 @@
of_nat_setsum [symmetric]
of_nat_eq_iff of_nat_id)
-subsection{* Pochhammer's symbol : generalized rising factorial
- See http://en.wikipedia.org/wiki/Pochhammer_symbol *}
+subsection{* Pochhammer's symbol : generalized rising factorial *}
+
+text {* See \url{http://en.wikipedia.org/wiki/Pochhammer_symbol} *}
definition "pochhammer (a::'a::comm_semiring_1) n =
(if n = 0 then 1 else setprod (\<lambda>n. a + of_nat n) {0 .. n - 1})"