16 |
16 |
17 const_maps |
17 const_maps |
18 "~" > "HOL.Not" |
18 "~" > "HOL.Not" |
19 "bool_case" > "Product_Type.bool.bool_case" |
19 "bool_case" > "Product_Type.bool.bool_case" |
20 "\\/" > "HOL.disj" |
20 "\\/" > "HOL.disj" |
21 "TYPE_DEFINITION" > "HOL4Setup.TYPE_DEFINITION" |
21 "TYPE_DEFINITION" > "Importer.TYPE_DEFINITION" |
22 "T" > "HOL.True" |
22 "T" > "HOL.True" |
23 "RES_SELECT" > "HOL4Base.bool.RES_SELECT" |
23 "RES_SELECT" > "HOL4Base.bool.RES_SELECT" |
24 "RES_FORALL" > "HOL4Base.bool.RES_FORALL" |
24 "RES_FORALL" > "HOL4Base.bool.RES_FORALL" |
25 "RES_EXISTS_UNIQUE" > "HOL4Base.bool.RES_EXISTS_UNIQUE" |
25 "RES_EXISTS_UNIQUE" > "HOL4Base.bool.RES_EXISTS_UNIQUE" |
26 "RES_EXISTS" > "HOL4Base.bool.RES_EXISTS" |
26 "RES_EXISTS" > "HOL4Base.bool.RES_EXISTS" |
27 "ONTO" > "Fun.surj" |
27 "ONTO" > "Fun.surj" |
28 "ONE_ONE" > "HOL4Setup.ONE_ONE" |
28 "ONE_ONE" > "Importer.ONE_ONE" |
29 "LET" > "Compatibility.LET" |
29 "LET" > "Compatibility.LET" |
30 "IN" > "HOL4Base.bool.IN" |
30 "IN" > "HOL4Base.bool.IN" |
31 "F" > "HOL.False" |
31 "F" > "HOL.False" |
32 "COND" > "HOL.If" |
32 "COND" > "HOL.If" |
33 "ARB" > "HOL4Base.bool.ARB" |
33 "ARB" > "HOL4Base.bool.ARB" |
47 "UNWIND_FORALL_THM2" > "HOL.simp_thms_41" |
47 "UNWIND_FORALL_THM2" > "HOL.simp_thms_41" |
48 "UNWIND_FORALL_THM1" > "HOL.simp_thms_42" |
48 "UNWIND_FORALL_THM1" > "HOL.simp_thms_42" |
49 "UEXISTS_SIMP" > "HOL4Base.bool.UEXISTS_SIMP" |
49 "UEXISTS_SIMP" > "HOL4Base.bool.UEXISTS_SIMP" |
50 "UEXISTS_OR_THM" > "HOL4Base.bool.UEXISTS_OR_THM" |
50 "UEXISTS_OR_THM" > "HOL4Base.bool.UEXISTS_OR_THM" |
51 "T_DEF" > "HOL.True_def" |
51 "T_DEF" > "HOL.True_def" |
52 "TYPE_DEFINITION_THM" > "HOL4Setup.TYPE_DEFINITION" |
52 "TYPE_DEFINITION_THM" > "Importer.TYPE_DEFINITION" |
53 "TYPE_DEFINITION" > "HOL4Setup.TYPE_DEFINITION" |
53 "TYPE_DEFINITION" > "Importer.TYPE_DEFINITION" |
54 "TRUTH" > "HOL.TrueI" |
54 "TRUTH" > "HOL.TrueI" |
55 "SWAP_FORALL_THM" > "HOL.all_comm" |
55 "SWAP_FORALL_THM" > "HOL.all_comm" |
56 "SWAP_EXISTS_THM" > "HOL.ex_comm" |
56 "SWAP_EXISTS_THM" > "HOL.ex_comm" |
57 "SKOLEM_THM" > "HOL4Base.bool.SKOLEM_THM" |
57 "SKOLEM_THM" > "HOL4Base.bool.SKOLEM_THM" |
58 "SELECT_UNIQUE" > "HOL4Base.bool.SELECT_UNIQUE" |
58 "SELECT_UNIQUE" > "HOL4Base.bool.SELECT_UNIQUE" |
59 "SELECT_THM" > "HOL4Setup.EXISTS_DEF" |
59 "SELECT_THM" > "Importer.EXISTS_DEF" |
60 "SELECT_REFL_2" > "Hilbert_Choice.some_sym_eq_trivial" |
60 "SELECT_REFL_2" > "Hilbert_Choice.some_sym_eq_trivial" |
61 "SELECT_REFL" > "Hilbert_Choice.some_eq_trivial" |
61 "SELECT_REFL" > "Hilbert_Choice.some_eq_trivial" |
62 "SELECT_AX" > "Hilbert_Choice.someI" |
62 "SELECT_AX" > "Hilbert_Choice.someI" |
63 "RIGHT_OR_OVER_AND" > "HOL.disj_conj_distribR" |
63 "RIGHT_OR_OVER_AND" > "HOL.disj_conj_distribR" |
64 "RIGHT_OR_EXISTS_THM" > "HOL.ex_simps_4" |
64 "RIGHT_OR_EXISTS_THM" > "HOL.ex_simps_4" |
86 "OR_CONG" > "HOL4Base.bool.OR_CONG" |
86 "OR_CONG" > "HOL4Base.bool.OR_CONG" |
87 "OR_CLAUSES" > "HOL4Base.bool.OR_CLAUSES" |
87 "OR_CLAUSES" > "HOL4Base.bool.OR_CLAUSES" |
88 "ONTO_THM" > "Fun.surj_def" |
88 "ONTO_THM" > "Fun.surj_def" |
89 "ONTO_DEF" > "Fun.surj_def" |
89 "ONTO_DEF" > "Fun.surj_def" |
90 "ONE_ONE_THM" > "HOL4Base.bool.ONE_ONE_THM" |
90 "ONE_ONE_THM" > "HOL4Base.bool.ONE_ONE_THM" |
91 "ONE_ONE_DEF" > "HOL4Setup.ONE_ONE_DEF" |
91 "ONE_ONE_DEF" > "Importer.ONE_ONE_DEF" |
92 "NOT_IMP" > "HOL.not_imp" |
92 "NOT_IMP" > "HOL.not_imp" |
93 "NOT_FORALL_THM" > "HOL.not_all" |
93 "NOT_FORALL_THM" > "HOL.not_all" |
94 "NOT_F" > "Groebner_Basis.PFalse_2" |
94 "NOT_F" > "Groebner_Basis.PFalse_2" |
95 "NOT_EXISTS_THM" > "HOL.not_ex" |
95 "NOT_EXISTS_THM" > "HOL.not_ex" |
96 "NOT_DEF" > "Groebner_Basis.bool_simps_19" |
96 "NOT_DEF" > "Groebner_Basis.bool_simps_19" |
116 "LEFT_EXISTS_AND_THM" > "HOL.ex_simps_1" |
116 "LEFT_EXISTS_AND_THM" > "HOL.ex_simps_1" |
117 "LEFT_AND_OVER_OR" > "Groebner_Basis.dnf_1" |
117 "LEFT_AND_OVER_OR" > "Groebner_Basis.dnf_1" |
118 "LEFT_AND_FORALL_THM" > "HOL.all_simps_1" |
118 "LEFT_AND_FORALL_THM" > "HOL.all_simps_1" |
119 "IN_def" > "HOL4Base.bool.IN_def" |
119 "IN_def" > "HOL4Base.bool.IN_def" |
120 "IN_DEF" > "HOL4Base.bool.IN_DEF" |
120 "IN_DEF" > "HOL4Base.bool.IN_DEF" |
121 "INFINITY_AX" > "HOL4Setup.INFINITY_AX" |
121 "INFINITY_AX" > "Importer.INFINITY_AX" |
122 "IMP_F_EQ_F" > "HOL4Base.bool.IMP_F_EQ_F" |
122 "IMP_F_EQ_F" > "HOL4Base.bool.IMP_F_EQ_F" |
123 "IMP_F" > "HOL.notI" |
123 "IMP_F" > "HOL.notI" |
124 "IMP_DISJ_THM" > "Groebner_Basis.nnf_simps_3" |
124 "IMP_DISJ_THM" > "Groebner_Basis.nnf_simps_3" |
125 "IMP_CONG" > "HOL.imp_cong" |
125 "IMP_CONG" > "HOL.imp_cong" |
126 "IMP_CLAUSES" > "HOL4Base.bool.IMP_CLAUSES" |
126 "IMP_CLAUSES" > "HOL4Base.bool.IMP_CLAUSES" |
138 "EXISTS_UNIQUE_DEF" > "Compatibility.EXISTS_UNIQUE_DEF" |
138 "EXISTS_UNIQUE_DEF" > "Compatibility.EXISTS_UNIQUE_DEF" |
139 "EXISTS_THM" > "HOL4Base.bool.EXISTS_THM" |
139 "EXISTS_THM" > "HOL4Base.bool.EXISTS_THM" |
140 "EXISTS_SIMP" > "HOL.simp_thms_36" |
140 "EXISTS_SIMP" > "HOL.simp_thms_36" |
141 "EXISTS_REFL" > "HOL.simp_thms_37" |
141 "EXISTS_REFL" > "HOL.simp_thms_37" |
142 "EXISTS_OR_THM" > "HOL.ex_disj_distrib" |
142 "EXISTS_OR_THM" > "HOL.ex_disj_distrib" |
143 "EXISTS_DEF" > "HOL4Setup.EXISTS_DEF" |
143 "EXISTS_DEF" > "Importer.EXISTS_DEF" |
144 "EXCLUDED_MIDDLE" > "HOL4Base.bool.EXCLUDED_MIDDLE" |
144 "EXCLUDED_MIDDLE" > "HOL4Base.bool.EXCLUDED_MIDDLE" |
145 "ETA_THM" > "HOL.eta_contract_eq" |
145 "ETA_THM" > "HOL.eta_contract_eq" |
146 "ETA_AX" > "HOL.eta_contract_eq" |
146 "ETA_AX" > "HOL.eta_contract_eq" |
147 "EQ_TRANS" > "HOL.trans" |
147 "EQ_TRANS" > "HOL.trans" |
148 "EQ_SYM_EQ" > "HOL.eq_ac_1" |
148 "EQ_SYM_EQ" > "HOL.eq_ac_1" |