author | wenzelm |
Tue, 08 Feb 2011 16:11:52 +0100 | |
changeset 41715 | 22f8c2483bd2 |
parent 41414 | 00b2b6716ed8 |
child 41886 | aa8dce9ab8a9 |
permissions | -rw-r--r-- |
27368 | 1 |
header {* Plain HOL *} |
2 |
||
3 |
theory Plain |
|
40178
00152d17855b
reverted e7a80c6752c9 -- there's not much point in putting a diagnosis tool (as opposed to a proof method) in Plain, but more importantly Sledgehammer must be in Main to use SMT solvers
blanchet
parents:
40121
diff
changeset
|
4 |
imports Datatype FunDef Extraction Metis |
27368 | 5 |
begin |
6 |
||
29304 | 7 |
text {* |
8 |
Plain bootstrap of fundamental HOL tools and packages; does not |
|
9 |
include @{text Hilbert_Choice}. |
|
10 |
*} |
|
11 |
||
41414
00b2b6716ed8
theory loader: implicit load path is considered legacy;
wenzelm
parents:
40178
diff
changeset
|
12 |
ML {* Thy_Load.legacy_path_add "~~/src/HOL/Library" *} |
27368 | 13 |
|
14 |
end |