1structure optionLib :> optionLib = 2struct 3 4 open Parse optionTheory optionSyntax; 5 6val option_rws = option_CLAUSES 7 8(* 9val OPTION_data = rewrites 10 (map ((fn th => if (is_neg (concl th)) then EQF_INTRO th else th) o SPEC_ALL) 11 (CONJUNCTS (theorem "option" "option_CLAUSES"))); 12 13in 14 15 val OPTION_ss = mk_simpset [OPTION_data]; 16 val option_ss = hol_ss ++ OPTION_data; 17 18end; 19*) 20 21val OPTION_rewrites = 22 [ THE_DEF, IS_SOME_DEF, IS_NONE_DEF, 23 SOME_11, NOT_NONE_SOME, NOT_SOME_NONE, 24 option_case_def, OPTION_MAP_DEF, 25 OPTION_BIND_def, OPTION_GUARD_def, 26 OPTION_IGNORE_BIND_def, OPTION_JOIN_DEF, OPTION_CHOICE_def, 27 OPTION_MAP2_THM]; 28 29val OPTION_rws = 30 computeLib.add_thms (List.map computeLib.lazyfy_thm OPTION_rewrites); 31 32end; 33