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

17658

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
