changeset 29609 | a010aab5bed0 |
parent 29304 | 5c71a6da989d |
child 29820 | 07f53494cf20 |
--- a/src/HOL/Plain.thy Wed Jan 21 23:40:23 2009 +0100 +++ b/src/HOL/Plain.thy Wed Jan 21 23:40:23 2009 +0100 @@ -1,7 +1,7 @@ header {* Plain HOL *} theory Plain -imports Datatype FunDef Record SAT Extraction +imports Datatype FunDef Record SAT Extraction Divides begin text {* @@ -9,6 +9,9 @@ include @{text Hilbert_Choice}. *} +instance option :: (finite) finite + by default (simp add: insert_None_conv_UNIV [symmetric]) + ML {* path_add "~~/src/HOL/Library" *} end