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