| changeset 16760 | 5c5f051aaaaa |
| parent 16733 | 236dfafbeb63 |
| child 16775 | c1b87ef4a1c3 |
| 16759:668e72b1c4d7 | 16760:5c5f051aaaaa |
|---|---|
5 *) |
5 *) |
6 |
6 |
7 header {* Finite sets *} |
7 header {* Finite sets *} |
8 |
8 |
9 theory Finite_Set |
9 theory Finite_Set |
10 imports Divides Power Inductive Lattice_Locales |
10 imports Power Inductive Lattice_Locales |
11 begin |
11 begin |
12 |
12 |
13 subsection {* Definition and basic properties *} |
13 subsection {* Definition and basic properties *} |
14 |
14 |
15 consts Finites :: "'a set set" |
15 consts Finites :: "'a set set" |