| changeset 24194 | 96013f81faef |
| parent 24163 | 9e6a2a7da86a |
| child 24267 | 867efa1dc4f8 |
| 24193:926dde4d96de | 24194:96013f81faef |
|---|---|
5 *) |
5 *) |
6 |
6 |
7 header {* Finite sets *} |
7 header {* Finite sets *} |
8 |
8 |
9 theory Finite_Set |
9 theory Finite_Set |
10 imports IntDef Divides Option |
10 imports IntDef Divides |
11 begin |
11 begin |
12 |
12 |
13 subsection {* Definition and basic properties *} |
13 subsection {* Definition and basic properties *} |
14 |
14 |
15 inductive finite :: "'a set => bool" |
15 inductive finite :: "'a set => bool" |