13 "nat_elim__magic" > "HOL4Base.arithmetic.nat_elim__magic" |
13 "nat_elim__magic" > "HOL4Base.arithmetic.nat_elim__magic" |
14 "NUMERAL_BIT2" > "HOL4Compat.NUMERAL_BIT2" |
14 "NUMERAL_BIT2" > "HOL4Compat.NUMERAL_BIT2" |
15 "NUMERAL_BIT1" > "HOL4Compat.NUMERAL_BIT1" |
15 "NUMERAL_BIT1" > "HOL4Compat.NUMERAL_BIT1" |
16 "NUMERAL" > "HOL4Compat.NUMERAL" |
16 "NUMERAL" > "HOL4Compat.NUMERAL" |
17 "MOD" > "Divides.op mod" :: "nat => nat => nat" |
17 "MOD" > "Divides.op mod" :: "nat => nat => nat" |
18 "MIN" > "HOL.min" :: "nat => nat => nat" |
18 "MIN" > "Orderings.min" :: "nat => nat => nat" |
19 "MAX" > "HOL.max" :: "nat => nat => nat" |
19 "MAX" > "Orderings.max" :: "nat => nat => nat" |
20 "FUNPOW" > "HOL4Compat.FUNPOW" |
20 "FUNPOW" > "HOL4Compat.FUNPOW" |
21 "EXP" > "Nat.power" :: "nat => nat => nat" |
21 "EXP" > "Nat.power" :: "nat => nat => nat" |
22 "DIV" > "Divides.op div" :: "nat => nat => nat" |
22 "DIV" > "Divides.op div" :: "nat => nat => nat" |
23 "ALT_ZERO" > "HOL4Compat.ALT_ZERO" |
23 "ALT_ZERO" > "HOL4Compat.ALT_ZERO" |
24 ">=" > "HOL4Compat.nat_ge" |
24 ">=" > "HOL4Compat.nat_ge" |
139 "MIN_MAX_PRED" > "HOL4Base.arithmetic.MIN_MAX_PRED" |
139 "MIN_MAX_PRED" > "HOL4Base.arithmetic.MIN_MAX_PRED" |
140 "MIN_MAX_LT" > "HOL4Base.arithmetic.MIN_MAX_LT" |
140 "MIN_MAX_LT" > "HOL4Base.arithmetic.MIN_MAX_LT" |
141 "MIN_MAX_EQ" > "HOL4Base.arithmetic.MIN_MAX_EQ" |
141 "MIN_MAX_EQ" > "HOL4Base.arithmetic.MIN_MAX_EQ" |
142 "MIN_LT" > "HOL4Base.arithmetic.MIN_LT" |
142 "MIN_LT" > "HOL4Base.arithmetic.MIN_LT" |
143 "MIN_LE" > "HOL4Base.arithmetic.MIN_LE" |
143 "MIN_LE" > "HOL4Base.arithmetic.MIN_LE" |
144 "MIN_IDEM" > "HOL.min_same" |
144 "MIN_IDEM" > "Orderings.min_same" |
145 "MIN_DEF" > "HOL4Compat.MIN_DEF" |
145 "MIN_DEF" > "HOL4Compat.MIN_DEF" |
146 "MIN_COMM" > "HOL.min_ac_2" |
146 "MIN_COMM" > "Orderings.min_ac_2" |
147 "MIN_ASSOC" > "HOL.min_ac_1" |
147 "MIN_ASSOC" > "Orderings.min_ac_1" |
148 "MIN_0" > "HOL4Base.arithmetic.MIN_0" |
148 "MIN_0" > "HOL4Base.arithmetic.MIN_0" |
149 "MAX_LT" > "HOL4Base.arithmetic.MAX_LT" |
149 "MAX_LT" > "HOL4Base.arithmetic.MAX_LT" |
150 "MAX_LE" > "HOL4Base.arithmetic.MAX_LE" |
150 "MAX_LE" > "HOL4Base.arithmetic.MAX_LE" |
151 "MAX_IDEM" > "HOL.max_same" |
151 "MAX_IDEM" > "Orderings.max_same" |
152 "MAX_DEF" > "HOL4Compat.MAX_DEF" |
152 "MAX_DEF" > "HOL4Compat.MAX_DEF" |
153 "MAX_COMM" > "HOL.max_ac_2" |
153 "MAX_COMM" > "Orderings.max_ac_2" |
154 "MAX_ASSOC" > "HOL.max_ac_1" |
154 "MAX_ASSOC" > "Orderings.max_ac_1" |
155 "MAX_0" > "HOL4Base.arithmetic.MAX_0" |
155 "MAX_0" > "HOL4Base.arithmetic.MAX_0" |
156 "LESS_TRANS" > "Nat.less_trans" |
156 "LESS_TRANS" > "Nat.less_trans" |
157 "LESS_SUC_NOT" > "HOL4Base.arithmetic.LESS_SUC_NOT" |
157 "LESS_SUC_NOT" > "HOL4Base.arithmetic.LESS_SUC_NOT" |
158 "LESS_SUC_EQ_COR" > "Nat.Suc_lessI" |
158 "LESS_SUC_EQ_COR" > "Nat.Suc_lessI" |
159 "LESS_SUB_ADD_LESS" > "HOL4Base.arithmetic.LESS_SUB_ADD_LESS" |
159 "LESS_SUB_ADD_LESS" > "HOL4Base.arithmetic.LESS_SUB_ADD_LESS" |
233 "EVEN_AND_ODD" > "HOL4Base.arithmetic.EVEN_AND_ODD" |
233 "EVEN_AND_ODD" > "HOL4Base.arithmetic.EVEN_AND_ODD" |
234 "EVEN_ADD" > "HOL4Base.arithmetic.EVEN_ADD" |
234 "EVEN_ADD" > "HOL4Base.arithmetic.EVEN_ADD" |
235 "EVEN" > "HOL4Base.arithmetic.EVEN" |
235 "EVEN" > "HOL4Base.arithmetic.EVEN" |
236 "EQ_MULT_LCANCEL" > "NatBin.nat_mult_eq_cancel_disj" |
236 "EQ_MULT_LCANCEL" > "NatBin.nat_mult_eq_cancel_disj" |
237 "EQ_MONO_ADD_EQ" > "Nat.nat_add_right_cancel" |
237 "EQ_MONO_ADD_EQ" > "Nat.nat_add_right_cancel" |
238 "EQ_LESS_EQ" > "HOL.order_eq_iff" |
238 "EQ_LESS_EQ" > "Orderings.order_eq_iff" |
239 "EQ_ADD_RCANCEL" > "Nat.nat_add_right_cancel" |
239 "EQ_ADD_RCANCEL" > "Nat.nat_add_right_cancel" |
240 "EQ_ADD_LCANCEL" > "Nat.nat_add_left_cancel" |
240 "EQ_ADD_LCANCEL" > "Nat.nat_add_left_cancel" |
241 "DIV_UNIQUE" > "HOL4Base.arithmetic.DIV_UNIQUE" |
241 "DIV_UNIQUE" > "HOL4Base.arithmetic.DIV_UNIQUE" |
242 "DIV_P" > "HOL4Base.arithmetic.DIV_P" |
242 "DIV_P" > "HOL4Base.arithmetic.DIV_P" |
243 "DIV_ONE" > "Divides.div_1" |
243 "DIV_ONE" > "Divides.div_1" |