equal
deleted
inserted
replaced
160 "LESS_OR_EQ_ADD" > "HOL4Base.arithmetic.LESS_OR_EQ_ADD" |
160 "LESS_OR_EQ_ADD" > "HOL4Base.arithmetic.LESS_OR_EQ_ADD" |
161 "LESS_OR_EQ" > "HOL4Compat.LESS_OR_EQ" |
161 "LESS_OR_EQ" > "HOL4Compat.LESS_OR_EQ" |
162 "LESS_OR" > "Nat.Suc_leI" |
162 "LESS_OR" > "Nat.Suc_leI" |
163 "LESS_NOT_SUC" > "HOL4Base.arithmetic.LESS_NOT_SUC" |
163 "LESS_NOT_SUC" > "HOL4Base.arithmetic.LESS_NOT_SUC" |
164 "LESS_MULT_MONO" > "Nat.Suc_mult_less_cancel1" |
164 "LESS_MULT_MONO" > "Nat.Suc_mult_less_cancel1" |
165 "LESS_MULT2" > "Ring_and_Field.mult_pos" |
165 "LESS_MULT2" > "Ring_and_Field.mult_pos_pos" |
166 "LESS_MONO_REV" > "Nat.Suc_less_SucD" |
166 "LESS_MONO_REV" > "Nat.Suc_less_SucD" |
167 "LESS_MONO_MULT" > "Nat.mult_le_mono1" |
167 "LESS_MONO_MULT" > "Nat.mult_le_mono1" |
168 "LESS_MONO_EQ" > "Nat.Suc_less_eq" |
168 "LESS_MONO_EQ" > "Nat.Suc_less_eq" |
169 "LESS_MONO_ADD_INV" > "OrderedGroup.add_less_imp_less_right" |
169 "LESS_MONO_ADD_INV" > "OrderedGroup.add_less_imp_less_right" |
170 "LESS_MONO_ADD_EQ" > "OrderedGroup.add_less_cancel_right" |
170 "LESS_MONO_ADD_EQ" > "OrderedGroup.add_less_cancel_right" |