| changeset 21249 | d594c58e24ed |
| parent 21215 | 7c9337a0e30a |
| child 21404 | eb85850d3eb7 |
| 21248:3fd22b0939ff | 21249:d594c58e24ed |
|---|---|
5 *) |
5 *) |
6 |
6 |
7 header {* Finite sets *} |
7 header {* Finite sets *} |
8 |
8 |
9 theory Finite_Set |
9 theory Finite_Set |
10 imports Power Inductive Lattice_Locales |
10 imports Power Inductive Lattices |
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" |