changeset 15382 | e56ce5cefe9c |
parent 15151 | 429666b09783 |
child 15395 | b93cdbac8f46 |
15381:780ea4c697f2 | 15382:e56ce5cefe9c |
---|---|
4 *) |
4 *) |
5 |
5 |
6 header {* Main HOL *} |
6 header {* Main HOL *} |
7 |
7 |
8 theory Main |
8 theory Main |
9 imports Map Infinite_Set Extraction Refute Reconstruction |
9 imports Extraction Refute Reconstruction |
10 |
10 |
11 begin |
11 begin |
12 |
12 |
13 text {* |
13 text {* |
14 Theory @{text Main} includes everything. Note that theory @{text |
14 Theory @{text Main} includes everything. Note that theory @{text |