1 import |
1 import |
2 |
2 |
3 import_segment "hol4" |
3 import_segment "hol4" |
4 |
4 |
5 type_maps |
5 type_maps |
6 "sum" > "+" |
6 "sum" > "Sum_Type.sum" |
7 |
7 |
8 const_maps |
8 const_maps |
9 "sum_case" > "Datatype.sum.sum_case" |
9 "sum_case" > "Sum_Type.sum.sum_case" |
10 "OUTR" > "HOL4Compat.OUTR" |
10 "OUTR" > "HOL4Compat.OUTR" |
11 "OUTL" > "HOL4Compat.OUTL" |
11 "OUTL" > "HOL4Compat.OUTL" |
12 "ISR" > "HOL4Compat.ISR" |
12 "ISR" > "HOL4Compat.ISR" |
13 "ISL" > "HOL4Compat.ISL" |
13 "ISL" > "HOL4Compat.ISL" |
14 "INR" > "Sum_Type.Inr" |
14 "INR" > "Sum_Type.Inr" |
15 "INL" > "Sum_Type.Inl" |
15 "INL" > "Sum_Type.Inl" |
16 |
16 |
17 thm_maps |
17 thm_maps |
18 "sum_distinct1" > "Datatype.sum.simps_2" |
18 "sum_distinct1" > "Sum_Type.Inr_not_Inl" |
19 "sum_distinct" > "Datatype.sum.simps_1" |
19 "sum_distinct" > "Sum_Type.Inl_not_Inr" |
20 "sum_case_def" > "HOL4Compat.sum_case_def" |
20 "sum_case_def" > "HOL4Compat.sum_case_def" |
21 "sum_case_cong" > "HOL4Base.sum.sum_case_cong" |
21 "sum_case_cong" > "HOL4Base.sum.sum_case_cong" |
22 "sum_INDUCT" > "HOL4Compat.OUTR.induct" |
22 "sum_axiom" > "HOL4Compat.sum_axiom" |
23 "sum_CASES" > "Datatype.sum.nchotomy" |
23 "sum_INDUCT" > "Sum_Type.sum.induct" |
|
24 "sum_CASES" > "Sum_Type.sum.nchotomy" |
24 "OUTR" > "HOL4Compat.OUTR" |
25 "OUTR" > "HOL4Compat.OUTR" |
25 "OUTL" > "HOL4Compat.OUTL" |
26 "OUTL" > "HOL4Compat.OUTL" |
26 "ISR" > "HOL4Compat.ISR" |
27 "ISR" > "HOL4Compat.ISR" |
27 "ISL_OR_ISR" > "HOL4Base.sum.ISL_OR_ISR" |
28 "ISL_OR_ISR" > "HOL4Base.sum.ISL_OR_ISR" |
28 "ISL" > "HOL4Compat.ISL" |
29 "ISL" > "HOL4Compat.ISL" |
29 "INR_neq_INL" > "Datatype.sum.simps_2" |
30 "INR_neq_INL" > "Sum_Type.Inr_not_Inl" |
30 "INR_INL_11" > "HOL4Compat.INR_INL_11" |
31 "INR_INL_11" > "HOL4Compat.INR_INL_11" |
31 "INR" > "HOL4Base.sum.INR" |
32 "INR" > "HOL4Base.sum.INR" |
32 "INL" > "HOL4Base.sum.INL" |
33 "INL" > "HOL4Base.sum.INL" |
33 |
34 |
34 ignore_thms |
35 ignore_thms |
35 "sum_axiom" |
|
36 "sum_TY_DEF" |
36 "sum_TY_DEF" |
37 "sum_ISO_DEF" |
37 "sum_ISO_DEF" |
38 "sum_Axiom" |
38 "sum_Axiom" |
39 "IS_SUM_REP" |
39 "IS_SUM_REP" |
40 "INR_DEF" |
40 "INR_DEF" |