equal
deleted
inserted
replaced
19 "CURRY" > "curry" |
19 "CURRY" > "curry" |
20 "," > "Pair" |
20 "," > "Pair" |
21 "##" > "prod_fun" |
21 "##" > "prod_fun" |
22 |
22 |
23 thm_maps |
23 thm_maps |
24 "pair_induction" > "Datatype.prod.induct" |
24 "pair_induction" > "Datatype.prod.induct_correctness" |
25 "pair_case_thm" > "Product_Type.split" |
25 "pair_case_thm" > "Product_Type.split" |
26 "pair_case_def" > "HOL4Compat.pair_case_def" |
26 "pair_case_def" > "HOL4Compat.pair_case_def" |
27 "pair_case_cong" > "HOL4Base.pair.pair_case_cong" |
27 "pair_case_cong" > "HOL4Base.pair.pair_case_cong" |
28 "pair_Axiom" > "HOL4Base.pair.pair_Axiom" |
28 "pair_Axiom" > "HOL4Base.pair.pair_Axiom" |
29 "WF_RPROD" > "HOL4Base.pair.WF_RPROD" |
29 "WF_RPROD" > "HOL4Base.pair.WF_RPROD" |