| changeset 15140 | 322485b816ac |
| parent 15131 | c69542757a4d |
| child 15228 | 4d332d10fa3d |
| 15139:58cd3404cf75 | 15140:322485b816ac |
|---|---|
5 *) |
5 *) |
6 |
6 |
7 header {* Finite sets *} |
7 header {* Finite sets *} |
8 |
8 |
9 theory Finite_Set |
9 theory Finite_Set |
10 import Divides Power Inductive |
10 imports Divides Power Inductive |
11 begin |
11 begin |
12 |
12 |
13 subsection {* Collection of finite sets *} |
13 subsection {* Collection of finite sets *} |
14 |
14 |
15 consts Finites :: "'a set set" |
15 consts Finites :: "'a set set" |