author | nipkow |
Sun, 22 Feb 2009 17:25:28 +0100 | |
changeset 30056 | 0a35bee25c20 |
parent 29837 | eb7e62c0f53c |
child 30073 | a4ad0c08b7d9 |
permissions | -rw-r--r-- |
27368 | 1 |
header {* Plain HOL *} |
2 |
||
3 |
theory Plain |
|
29837
eb7e62c0f53c
Now imports Fact as suggested by Florian in order to avoid the typerep problem
chaieb
parents:
29820
diff
changeset
|
4 |
imports Datatype FunDef Record Extraction Divides Fact |
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 |