equal
deleted
inserted
replaced
500 qed |
500 qed |
501 |
501 |
502 |
502 |
503 subsection \<open>Pochhammer's symbol: generalized rising factorial\<close> |
503 subsection \<open>Pochhammer's symbol: generalized rising factorial\<close> |
504 |
504 |
505 text \<open>See @{url "http://en.wikipedia.org/wiki/Pochhammer_symbol"}\<close> |
505 text \<open>See \<^url>\<open>http://en.wikipedia.org/wiki/Pochhammer_symbol\<close>.\<close> |
506 |
506 |
507 context comm_semiring_1 |
507 context comm_semiring_1 |
508 begin |
508 begin |
509 |
509 |
510 definition pochhammer :: "'a \<Rightarrow> nat \<Rightarrow> 'a" |
510 definition pochhammer :: "'a \<Rightarrow> nat \<Rightarrow> 'a" |