| changeset 15140 | 322485b816ac |
| parent 15131 | c69542757a4d |
| child 15151 | 429666b09783 |
| 15139:58cd3404cf75 | 15140:322485b816ac |
|---|---|
4 *) |
4 *) |
5 |
5 |
6 header {* Main HOL *} |
6 header {* Main HOL *} |
7 |
7 |
8 theory Main |
8 theory Main |
9 import Map Infinite_Set Extraction Refute |
9 imports Map Infinite_Set Extraction Refute |
10 begin |
10 begin |
11 |
11 |
12 text {* |
12 text {* |
13 Theory @{text Main} includes everything. Note that theory @{text |
13 Theory @{text Main} includes everything. Note that theory @{text |
14 PreList} already includes most HOL theories. |
14 PreList} already includes most HOL theories. |