author | huffman |
Tue, 24 Feb 2009 11:12:58 -0800 | |
changeset 30082 | 43c5b7bfc791 |
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 |