equal
deleted
inserted
replaced
1 (* Title: HOL/Plain.thy |
|
2 ID: $Id$ |
|
3 |
|
4 Contains fundamental HOL tools and packages. Does not include Hilbert_Choice. |
|
5 *) |
|
6 |
|
7 header {* Plain HOL *} |
1 header {* Plain HOL *} |
8 |
2 |
9 theory Plain |
3 theory Plain |
10 imports Datatype FunDef Record SAT Extraction |
4 imports Datatype FunDef Record SAT Extraction |
11 begin |
5 begin |
12 |
6 |
|
7 text {* |
|
8 Plain bootstrap of fundamental HOL tools and packages; does not |
|
9 include @{text Hilbert_Choice}. |
|
10 *} |
|
11 |
13 ML {* path_add "~~/src/HOL/Library" *} |
12 ML {* path_add "~~/src/HOL/Library" *} |
14 |
13 |
15 end |
14 end |