changeset 15872 | 8336ff711d80 |
parent 15584 | 3478bb4f93ff |
child 15965 | f422f8283491 |
15871:e524119dbf19 | 15872:8336ff711d80 |
---|---|
4 *) |
4 *) |
5 |
5 |
6 header {* Main HOL *} |
6 header {* Main HOL *} |
7 |
7 |
8 theory Main |
8 theory Main |
9 imports Extraction Refute Reconstruction |
9 imports 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 |