| author | nipkow |
| Fri, 13 Feb 2009 23:55:04 +0100 | |
| changeset 29901 | f4b3f8fbf599 |
| parent 29837 | eb7e62c0f53c |
| child 30073 | a4ad0c08b7d9 |
| permissions | -rw-r--r-- |
header {* Plain HOL *} theory Plain imports Datatype FunDef Record Extraction Divides Fact begin text {* Plain bootstrap of fundamental HOL tools and packages; does not include @{text Hilbert_Choice}. *} instance option :: (finite) finite by default (simp add: insert_None_conv_UNIV [symmetric]) ML {* path_add "~~/src/HOL/Library" *} end