equal
deleted
inserted
replaced
6 *) |
6 *) |
7 |
7 |
8 section \<open>Stirling numbers of first and second kind\<close> |
8 section \<open>Stirling numbers of first and second kind\<close> |
9 |
9 |
10 theory Stirling |
10 theory Stirling |
11 imports Binomial |
11 imports Main |
12 begin |
12 begin |
13 |
13 |
14 subsection \<open>Stirling numbers of the second kind\<close> |
14 subsection \<open>Stirling numbers of the second kind\<close> |
15 |
15 |
16 fun Stirling :: "nat \<Rightarrow> nat \<Rightarrow> nat" |
16 fun Stirling :: "nat \<Rightarrow> nat \<Rightarrow> nat" |