author | blanchet |
Wed, 15 Dec 2010 11:26:28 +0100 | |
changeset 41140 | 9c68004b8c9d |
parent 40178 | 00152d17855b |
child 41414 | 00b2b6716ed8 |
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 |
||
27368 | 12 |
ML {* path_add "~~/src/HOL/Library" *} |
13 |
||
14 |
end |