# HG changeset patch
# User wenzelm
# Date 1386417151 -3600
# Node ID ecaf646b865ac26f5eaa4a5a7e9b2abcdc1e4a2d
# Parent  47e61b768814f9d7a46f41c56b510a6e291c8419
proper latex;

diff -r 47e61b768814 -r ecaf646b865a src/HOL/Library/Binomial.thy
--- 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})"