| changeset 63680 | 6e1e8b5abbfa |
| parent 63648 | f9f3006a5579 |
| child 63725 | 4c00ba1ad11a |
--- a/src/HOL/Binomial.thy Fri Aug 12 17:49:02 2016 +0200 +++ b/src/HOL/Binomial.thy Fri Aug 12 17:53:55 2016 +0200 @@ -502,7 +502,7 @@ subsection \<open>Pochhammer's symbol: generalized rising factorial\<close> -text \<open>See @{url "http://en.wikipedia.org/wiki/Pochhammer_symbol"}\<close> +text \<open>See \<^url>\<open>http://en.wikipedia.org/wiki/Pochhammer_symbol\<close>.\<close> context comm_semiring_1 begin