| changeset 20809 | 6c4fd0b4b63a |
| parent 20369 | 7e03c3ed1a18 |
| child 22274 | ce1459004c8d |
| 20808:96d413f78870 | 20809:6c4fd0b4b63a |
|---|---|
4 *) |
4 *) |
5 |
5 |
6 header {*Finite Sets and Finite Sums*} |
6 header {*Finite Sets and Finite Sums*} |
7 |
7 |
8 theory Finite2 |
8 theory Finite2 |
9 imports IntFact |
9 imports IntFact Infinite_Set |
10 begin |
10 begin |
11 |
11 |
12 text{* |
12 text{* |
13 These are useful for combinatorial and number-theoretic counting |
13 These are useful for combinatorial and number-theoretic counting |
14 arguments. |
14 arguments. |