9 "sum_case" > "Datatype.sum.sum_case" |
9 "sum_case" > "Datatype.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" > "Inr" |
14 "INR" > "Sum_Type.Inr" |
15 "INL" > "Inl" |
15 "INL" > "Sum_Type.Inl" |
16 |
16 |
17 thm_maps |
17 thm_maps |
18 "sum_distinct1" > "Sum_Type.Inr_not_Inl" |
18 "sum_distinct1" > "Datatype.sum.simps_2" |
19 "sum_distinct" > "Sum_Type.Inl_not_Inr" |
19 "sum_distinct" > "Datatype.sum.simps_1" |
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_INDUCT" > "HOL4Compat.OUTR.induct" |
23 "sum_CASES" > "Datatype.sum.nchotomy" |
23 "sum_CASES" > "Datatype.sum.nchotomy" |
24 "OUTR" > "HOL4Compat.OUTR" |
24 "OUTR" > "HOL4Compat.OUTR" |
25 "OUTL" > "HOL4Compat.OUTL" |
25 "OUTL" > "HOL4Compat.OUTL" |
26 "ISR" > "HOL4Compat.ISR" |
26 "ISR" > "HOL4Compat.ISR" |
27 "ISL_OR_ISR" > "HOL4Base.sum.ISL_OR_ISR" |
27 "ISL_OR_ISR" > "HOL4Base.sum.ISL_OR_ISR" |
28 "ISL" > "HOL4Compat.ISL" |
28 "ISL" > "HOL4Compat.ISL" |
29 "INR_neq_INL" > "Sum_Type.Inr_not_Inl" |
29 "INR_neq_INL" > "Datatype.sum.simps_2" |
30 "INR_INL_11" > "HOL4Compat.INR_INL_11" |
30 "INR_INL_11" > "HOL4Compat.INR_INL_11" |
31 "INR" > "HOL4Base.sum.INR" |
31 "INR" > "HOL4Base.sum.INR" |
32 "INL" > "HOL4Base.sum.INL" |
32 "INL" > "HOL4Base.sum.INL" |
33 |
33 |
34 ignore_thms |
34 ignore_thms |