1 import |
1 import |
2 |
2 |
3 import_segment "hol4" |
3 import_segment "hol4" |
4 |
4 |
5 type_maps |
5 type_maps |
6 "option" > "Datatype.option" |
6 "option" > "Option.option" |
7 |
7 |
8 const_maps |
8 const_maps |
9 "option_case" > "Datatype.option.option_case" |
9 "option_case" > "Option.option.option_case" |
10 "THE" > "Datatype.the" |
10 "THE" > "Option.the" |
11 "SOME" > "Datatype.option.Some" |
11 "SOME" > "Option.option.Some" |
12 "OPTION_MAP" > "Datatype.option_map" |
12 "OPTION_MAP" > "Option.map" |
13 "OPTION_JOIN" > "HOL4Compat.OPTION_JOIN" |
13 "OPTION_JOIN" > "HOL4Compat.OPTION_JOIN" |
14 "NONE" > "Datatype.option.None" |
14 "NONE" > "Option.option.None" |
15 "IS_SOME" > "HOL4Compat.IS_SOME" |
15 "IS_SOME" > "HOL4Compat.IS_SOME" |
16 "IS_NONE" > "HOL4Compat.IS_NONE" |
16 "IS_NONE" > "HOL4Compat.IS_NONE" |
17 |
17 |
18 thm_maps |
18 thm_maps |
19 "option_nchotomy" > "Datatype.option.nchotomy" |
19 "option_nchotomy" > "Option.option.nchotomy" |
20 "option_induction" > "HOL4Compat.OPTION_JOIN.induct" |
20 "option_induction" > "Option.option.induct" |
21 "option_case_def" > "HOL4Compat.option_case_def" |
21 "option_case_def" > "HOL4Compat.option_case_def" |
22 "option_case_cong" > "HOL4Base.option.option_case_cong" |
22 "option_case_cong" > "HOL4Base.option.option_case_cong" |
23 "option_case_compute" > "HOL4Base.option.option_case_compute" |
23 "option_case_compute" > "HOL4Base.option.option_case_compute" |
24 "option_CLAUSES" > "HOL4Base.option.option_CLAUSES" |
24 "option_CLAUSES" > "HOL4Base.option.option_CLAUSES" |
25 "THE_DEF" > "Datatype.the.simps" |
25 "THE_DEF" > "Option.the.simps" |
26 "SOME_11" > "Datatype.option.simps_3" |
26 "SOME_11" > "Option.option.inject" |
27 "OPTION_MAP_EQ_SOME" > "HOL4Base.option.OPTION_MAP_EQ_SOME" |
27 "OPTION_MAP_EQ_SOME" > "HOL4Base.option.OPTION_MAP_EQ_SOME" |
28 "OPTION_MAP_EQ_NONE" > "Datatype.option_map_is_None" |
28 "OPTION_MAP_EQ_NONE" > "Option.option_map_is_None" |
29 "OPTION_MAP_DEF" > "HOL4Compat.OPTION_MAP_DEF" |
29 "OPTION_MAP_DEF" > "HOL4Compat.OPTION_MAP_DEF" |
30 "OPTION_JOIN_EQ_SOME" > "HOL4Base.option.OPTION_JOIN_EQ_SOME" |
30 "OPTION_JOIN_EQ_SOME" > "HOL4Base.option.OPTION_JOIN_EQ_SOME" |
31 "OPTION_JOIN_DEF" > "HOL4Compat.OPTION_JOIN_DEF" |
31 "OPTION_JOIN_DEF" > "HOL4Compat.OPTION_JOIN_DEF" |
32 "NOT_SOME_NONE" > "Datatype.option.simps_2" |
32 "NOT_SOME_NONE" > "Option.option.distinct_2" |
33 "NOT_NONE_SOME" > "Datatype.option.simps_1" |
33 "NOT_NONE_SOME" > "Option.option.distinct_1" |
34 "IS_SOME_DEF" > "HOL4Compat.IS_SOME_DEF" |
34 "IS_SOME_DEF" > "HOL4Compat.IS_SOME_DEF" |
35 "IS_NONE_DEF" > "HOL4Compat.IS_NONE_DEF" |
35 "IS_NONE_DEF" > "HOL4Compat.IS_NONE_DEF" |
36 |
36 |
37 ignore_thms |
37 ignore_thms |
38 "option_axiom" |
38 "option_axiom" |