| changeset 27487 | c8a6ce181805 |
| parent 27368 | 9f90ac19e32b |
| child 29694 | 2f2558d7bc3e |
| 27486:c61507a98bff | 27487:c8a6ce181805 |
|---|---|
5 *) |
5 *) |
6 |
6 |
7 header {* Binomial Coefficients *} |
7 header {* Binomial Coefficients *} |
8 |
8 |
9 theory Binomial |
9 theory Binomial |
10 imports Plain SetInterval |
10 imports Plain "~~/src/HOL/SetInterval" |
11 begin |
11 begin |
12 |
12 |
13 text {* This development is based on the work of Andy Gordon and |
13 text {* This development is based on the work of Andy Gordon and |
14 Florian Kammueller. *} |
14 Florian Kammueller. *} |
15 |
15 |