author | blanchet |
Fri, 06 Mar 2009 15:54:33 +0100 | |
changeset 30311 | 66a57e4f043e |
parent 30073 | a4ad0c08b7d9 |
child 30327 | 4d1185c77f4a |
permissions | -rw-r--r-- |
27368 | 1 |
header {* Plain HOL *} |
2 |
||
3 |
theory Plain |
|
30073 | 4 |
imports Datatype FunDef Record Extraction Divides |
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 |
||
29609 | 12 |
instance option :: (finite) finite |
13 |
by default (simp add: insert_None_conv_UNIV [symmetric]) |
|
14 |
||
27368 | 15 |
ML {* path_add "~~/src/HOL/Library" *} |
16 |
||
17 |
end |