| changeset 24280 | c9867bdf2424 |
| parent 23878 | bd651ecd4b8a |
| child 24286 | 7619080e49f0 |
| 24279:165648d5679f | 24280:c9867bdf2424 |
|---|---|
4 *) |
4 *) |
5 |
5 |
6 header {* Set theory for higher-order logic *} |
6 header {* Set theory for higher-order logic *} |
7 |
7 |
8 theory Set |
8 theory Set |
9 imports HOL |
9 imports Code_Setup |
10 begin |
10 begin |
11 |
11 |
12 text {* A set in HOL is simply a predicate. *} |
12 text {* A set in HOL is simply a predicate. *} |
13 |
13 |
14 |
14 |