|
14516
|
1 |
import
|
|
|
2 |
|
|
|
3 |
import_segment "hol4"
|
|
|
4 |
|
|
|
5 |
def_maps
|
|
|
6 |
"RPROD" > "RPROD_def"
|
|
|
7 |
"LEX" > "LEX_def"
|
|
|
8 |
|
|
|
9 |
type_maps
|
|
|
10 |
"prod" > "*"
|
|
|
11 |
|
|
|
12 |
const_maps
|
|
|
13 |
"pair_case" > "split"
|
|
|
14 |
"UNCURRY" > "split"
|
|
|
15 |
"SND" > "snd"
|
|
|
16 |
"RPROD" > "HOL4Base.pair.RPROD"
|
|
|
17 |
"LEX" > "HOL4Base.pair.LEX"
|
|
|
18 |
"FST" > "fst"
|
|
|
19 |
"CURRY" > "curry"
|
|
|
20 |
"," > "Pair"
|
|
|
21 |
"##" > "prod_fun"
|
|
|
22 |
|
|
|
23 |
thm_maps
|
|
17727
|
24 |
"pair_induction" > "Datatype.prod.induct_correctness"
|
|
14516
|
25 |
"pair_case_thm" > "Product_Type.split"
|
|
|
26 |
"pair_case_def" > "HOL4Compat.pair_case_def"
|
|
|
27 |
"pair_case_cong" > "HOL4Base.pair.pair_case_cong"
|
|
|
28 |
"pair_Axiom" > "HOL4Base.pair.pair_Axiom"
|
|
|
29 |
"WF_RPROD" > "HOL4Base.pair.WF_RPROD"
|
|
|
30 |
"WF_LEX" > "HOL4Base.pair.WF_LEX"
|
|
|
31 |
"UNCURRY_VAR" > "Product_Type.split_beta"
|
|
|
32 |
"UNCURRY_ONE_ONE_THM" > "HOL4Base.pair.UNCURRY_ONE_ONE_THM"
|
|
|
33 |
"UNCURRY_DEF" > "Product_Type.split"
|
|
|
34 |
"UNCURRY_CURRY_THM" > "Product_Type.split_curry"
|
|
|
35 |
"UNCURRY_CONG" > "HOL4Base.pair.UNCURRY_CONG"
|
|
|
36 |
"UNCURRY" > "Product_Type.split_beta"
|
|
|
37 |
"SND" > "Product_Type.snd_conv"
|
|
|
38 |
"RPROD_def" > "HOL4Base.pair.RPROD_def"
|
|
|
39 |
"RPROD_DEF" > "HOL4Base.pair.RPROD_DEF"
|
|
|
40 |
"PFORALL_THM" > "HOL4Base.pair.PFORALL_THM"
|
|
|
41 |
"PEXISTS_THM" > "HOL4Base.pair.PEXISTS_THM"
|
|
|
42 |
"PAIR_MAP_THM" > "Product_Type.prod_fun"
|
|
|
43 |
"PAIR_MAP" > "HOL4Compat.PAIR_MAP"
|
|
15647
|
44 |
"PAIR_EQ" > "Datatype.prod.simps_1"
|
|
14516
|
45 |
"PAIR" > "HOL4Compat.PAIR"
|
|
|
46 |
"LEX_def" > "HOL4Base.pair.LEX_def"
|
|
|
47 |
"LEX_DEF" > "HOL4Base.pair.LEX_DEF"
|
|
|
48 |
"LET2_RATOR" > "HOL4Base.pair.LET2_RATOR"
|
|
|
49 |
"LET2_RAND" > "HOL4Base.pair.LET2_RAND"
|
|
|
50 |
"LAMBDA_PROD" > "Product_Type.split_eta"
|
|
|
51 |
"FST" > "Product_Type.fst_conv"
|
|
|
52 |
"FORALL_PROD" > "Product_Type.split_paired_All"
|
|
|
53 |
"EXISTS_PROD" > "Product_Type.split_paired_Ex"
|
|
|
54 |
"ELIM_UNCURRY" > "Product_Type.split_beta"
|
|
|
55 |
"ELIM_PFORALL" > "HOL4Base.pair.ELIM_PFORALL"
|
|
|
56 |
"ELIM_PEXISTS" > "HOL4Base.pair.ELIM_PEXISTS"
|
|
|
57 |
"CURRY_UNCURRY_THM" > "Product_Type.curry_split"
|
|
|
58 |
"CURRY_ONE_ONE_THM" > "HOL4Base.pair.CURRY_ONE_ONE_THM"
|
|
|
59 |
"CURRY_DEF" > "Product_Type.curry_conv"
|
|
15647
|
60 |
"CLOSED_PAIR_EQ" > "Datatype.prod.simps_1"
|
|
|
61 |
"ABS_PAIR_THM" > "Datatype.prod.nchotomy"
|
|
14516
|
62 |
|
|
|
63 |
ignore_thms
|
|
|
64 |
"prod_TY_DEF"
|
|
|
65 |
"MK_PAIR_DEF"
|
|
|
66 |
"IS_PAIR_DEF"
|
|
|
67 |
"COMMA_DEF"
|
|
|
68 |
"ABS_REP_prod"
|
|
|
69 |
|
|
|
70 |
end
|