| changeset 27368 | 9f90ac19e32b |
| child 29304 | 5c71a6da989d |
| 27367:a75d71c73362 | 27368:9f90ac19e32b |
|---|---|
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 *} |
|
8 |
|
9 theory Plain |
|
10 imports Datatype FunDef Record SAT Extraction |
|
11 begin |
|
12 |
|
13 ML {* path_add "~~/src/HOL/Library" *} |
|
14 |
|
15 end |