45 "SUC_SUB1" > "HOL4Base.arithmetic.SUC_SUB1" |
45 "SUC_SUB1" > "HOL4Base.arithmetic.SUC_SUB1" |
46 "SUC_ONE_ADD" > "NatBin.Suc_eq_add_numeral_1_left" |
46 "SUC_ONE_ADD" > "NatBin.Suc_eq_add_numeral_1_left" |
47 "SUC_NOT" > "Nat.nat.simps_2" |
47 "SUC_NOT" > "Nat.nat.simps_2" |
48 "SUC_ELIM_THM" > "HOL4Base.arithmetic.SUC_ELIM_THM" |
48 "SUC_ELIM_THM" > "HOL4Base.arithmetic.SUC_ELIM_THM" |
49 "SUC_ADD_SYM" > "HOL4Base.arithmetic.SUC_ADD_SYM" |
49 "SUC_ADD_SYM" > "HOL4Base.arithmetic.SUC_ADD_SYM" |
50 "SUB_SUB" > "NatArith.diff_diff_right" |
50 "SUB_SUB" > "Nat.diff_diff_right" |
51 "SUB_RIGHT_SUB" > "Nat.diff_diff_left" |
51 "SUB_RIGHT_SUB" > "Nat.diff_diff_left" |
52 "SUB_RIGHT_LESS_EQ" > "HOL4Base.arithmetic.SUB_RIGHT_LESS_EQ" |
52 "SUB_RIGHT_LESS_EQ" > "HOL4Base.arithmetic.SUB_RIGHT_LESS_EQ" |
53 "SUB_RIGHT_LESS" > "HOL4Base.arithmetic.SUB_RIGHT_LESS" |
53 "SUB_RIGHT_LESS" > "HOL4Base.arithmetic.SUB_RIGHT_LESS" |
54 "SUB_RIGHT_GREATER_EQ" > "HOL4Base.arithmetic.SUB_RIGHT_GREATER_EQ" |
54 "SUB_RIGHT_GREATER_EQ" > "HOL4Base.arithmetic.SUB_RIGHT_GREATER_EQ" |
55 "SUB_RIGHT_GREATER" > "HOL4Base.arithmetic.SUB_RIGHT_GREATER" |
55 "SUB_RIGHT_GREATER" > "HOL4Base.arithmetic.SUB_RIGHT_GREATER" |
62 "SUB_LESS_EQ" > "Nat.diff_le_self" |
62 "SUB_LESS_EQ" > "Nat.diff_le_self" |
63 "SUB_LESS_0" > "Nat.zero_less_diff" |
63 "SUB_LESS_0" > "Nat.zero_less_diff" |
64 "SUB_LEFT_SUC" > "HOL4Base.arithmetic.SUB_LEFT_SUC" |
64 "SUB_LEFT_SUC" > "HOL4Base.arithmetic.SUB_LEFT_SUC" |
65 "SUB_LEFT_SUB" > "HOL4Base.arithmetic.SUB_LEFT_SUB" |
65 "SUB_LEFT_SUB" > "HOL4Base.arithmetic.SUB_LEFT_SUB" |
66 "SUB_LEFT_LESS_EQ" > "HOL4Base.arithmetic.SUB_LEFT_LESS_EQ" |
66 "SUB_LEFT_LESS_EQ" > "HOL4Base.arithmetic.SUB_LEFT_LESS_EQ" |
67 "SUB_LEFT_LESS" > "NatArith.less_diff_conv" |
67 "SUB_LEFT_LESS" > "Nat.less_diff_conv" |
68 "SUB_LEFT_GREATER_EQ" > "NatArith.le_diff_conv" |
68 "SUB_LEFT_GREATER_EQ" > "Nat.le_diff_conv" |
69 "SUB_LEFT_GREATER" > "HOL4Base.arithmetic.SUB_LEFT_GREATER" |
69 "SUB_LEFT_GREATER" > "HOL4Base.arithmetic.SUB_LEFT_GREATER" |
70 "SUB_LEFT_EQ" > "HOL4Base.arithmetic.SUB_LEFT_EQ" |
70 "SUB_LEFT_EQ" > "HOL4Base.arithmetic.SUB_LEFT_EQ" |
71 "SUB_LEFT_ADD" > "HOL4Base.arithmetic.SUB_LEFT_ADD" |
71 "SUB_LEFT_ADD" > "HOL4Base.arithmetic.SUB_LEFT_ADD" |
72 "SUB_EQ_EQ_0" > "HOL4Base.arithmetic.SUB_EQ_EQ_0" |
72 "SUB_EQ_EQ_0" > "HOL4Base.arithmetic.SUB_EQ_EQ_0" |
73 "SUB_EQ_0" > "Nat.diff_is_0_eq" |
73 "SUB_EQ_0" > "Nat.diff_is_0_eq" |
183 "LESS_EQ_MONO_ADD_EQ" > "OrderedGroup.add_le_cancel_right" |
183 "LESS_EQ_MONO_ADD_EQ" > "OrderedGroup.add_le_cancel_right" |
184 "LESS_EQ_MONO" > "Nat.Suc_le_mono" |
184 "LESS_EQ_MONO" > "Nat.Suc_le_mono" |
185 "LESS_EQ_LESS_TRANS" > "Nat.le_less_trans" |
185 "LESS_EQ_LESS_TRANS" > "Nat.le_less_trans" |
186 "LESS_EQ_LESS_EQ_MONO" > "Nat.add_le_mono" |
186 "LESS_EQ_LESS_EQ_MONO" > "Nat.add_le_mono" |
187 "LESS_EQ_IMP_LESS_SUC" > "Nat.le_imp_less_Suc" |
187 "LESS_EQ_IMP_LESS_SUC" > "Nat.le_imp_less_Suc" |
188 "LESS_EQ_EXISTS" > "NatArith.le_iff_add" |
188 "LESS_EQ_EXISTS" > "Nat.le_iff_add" |
189 "LESS_EQ_CASES" > "Nat.nat_le_linear" |
189 "LESS_EQ_CASES" > "Nat.nat_le_linear" |
190 "LESS_EQ_ANTISYM" > "HOL4Base.arithmetic.LESS_EQ_ANTISYM" |
190 "LESS_EQ_ANTISYM" > "HOL4Base.arithmetic.LESS_EQ_ANTISYM" |
191 "LESS_EQ_ADD_SUB" > "NatArith.add_diff_assoc" |
191 "LESS_EQ_ADD_SUB" > "Nat.add_diff_assoc" |
192 "LESS_EQ_ADD" > "Nat.le_add1" |
192 "LESS_EQ_ADD" > "Nat.le_add1" |
193 "LESS_EQ_0" > "Nat.le_0_eq" |
193 "LESS_EQ_0" > "Nat.le_0_eq" |
194 "LESS_EQUAL_ANTISYM" > "Nat.le_anti_sym" |
194 "LESS_EQUAL_ANTISYM" > "Nat.le_anti_sym" |
195 "LESS_EQUAL_ADD" > "HOL4Base.arithmetic.LESS_EQUAL_ADD" |
195 "LESS_EQUAL_ADD" > "HOL4Base.arithmetic.LESS_EQUAL_ADD" |
196 "LESS_EQ" > "Nat.le_simps_3" |
196 "LESS_EQ" > "Nat.le_simps_3" |
247 "DIV_DIV_DIV_MULT" > "HOL4Base.arithmetic.DIV_DIV_DIV_MULT" |
247 "DIV_DIV_DIV_MULT" > "HOL4Base.arithmetic.DIV_DIV_DIV_MULT" |
248 "DIVMOD_ID" > "HOL4Base.arithmetic.DIVMOD_ID" |
248 "DIVMOD_ID" > "HOL4Base.arithmetic.DIVMOD_ID" |
249 "DIVISION" > "HOL4Compat.DIVISION" |
249 "DIVISION" > "HOL4Compat.DIVISION" |
250 "DA" > "HOL4Base.arithmetic.DA" |
250 "DA" > "HOL4Base.arithmetic.DA" |
251 "COMPLETE_INDUCTION" > "Nat.less_induct" |
251 "COMPLETE_INDUCTION" > "Nat.less_induct" |
252 "CANCEL_SUB" > "NatArith.eq_diff_iff" |
252 "CANCEL_SUB" > "Nat.eq_diff_iff" |
253 "ALT_ZERO" > "HOL4Compat.ALT_ZERO_def" |
253 "ALT_ZERO" > "HOL4Compat.ALT_ZERO_def" |
254 "ADD_SYM" > "Finite_Set.AC_add.f.AC_2" |
254 "ADD_SYM" > "Finite_Set.AC_add.f.AC_2" |
255 "ADD_SUC" > "Nat.add_Suc_right" |
255 "ADD_SUC" > "Nat.add_Suc_right" |
256 "ADD_SUB" > "Nat.diff_add_inverse2" |
256 "ADD_SUB" > "Nat.diff_add_inverse2" |
257 "ADD_MONO_LESS_EQ" > "Nat.nat_add_left_cancel_le" |
257 "ADD_MONO_LESS_EQ" > "Nat.nat_add_left_cancel_le" |