145 "REAL_MEAN" > "Ring_and_Field.dense" |
145 "REAL_MEAN" > "Ring_and_Field.dense" |
146 "REAL_LT_TRANS" > "Set.basic_trans_rules_21" |
146 "REAL_LT_TRANS" > "Set.basic_trans_rules_21" |
147 "REAL_LT_TOTAL" > "HOL4Compat.REAL_LT_TOTAL" |
147 "REAL_LT_TOTAL" > "HOL4Compat.REAL_LT_TOTAL" |
148 "REAL_LT_SUB_RADD" > "OrderedGroup.compare_rls_6" |
148 "REAL_LT_SUB_RADD" > "OrderedGroup.compare_rls_6" |
149 "REAL_LT_SUB_LADD" > "OrderedGroup.compare_rls_7" |
149 "REAL_LT_SUB_LADD" > "OrderedGroup.compare_rls_7" |
150 "REAL_LT_RMUL_IMP" > "Ring_and_Field.ordered_semiring_strict_class.mult_strict_right_mono" |
150 "REAL_LT_RMUL_IMP" > "Ring_and_Field.mult_strict_right_mono" |
151 "REAL_LT_RMUL_0" > "HOL4Real.real.REAL_LT_RMUL_0" |
151 "REAL_LT_RMUL_0" > "HOL4Real.real.REAL_LT_RMUL_0" |
152 "REAL_LT_RMUL" > "RealDef.real_mult_less_iff1" |
152 "REAL_LT_RMUL" > "RealDef.real_mult_less_iff1" |
153 "REAL_LT_REFL" > "Orderings.order_less_irrefl" |
153 "REAL_LT_REFL" > "Orderings.order_less_irrefl" |
154 "REAL_LT_RDIV_EQ" > "Ring_and_Field.pos_less_divide_eq" |
154 "REAL_LT_RDIV_EQ" > "Ring_and_Field.pos_less_divide_eq" |
155 "REAL_LT_RDIV_0" > "HOL4Real.real.REAL_LT_RDIV_0" |
155 "REAL_LT_RDIV_0" > "HOL4Real.real.REAL_LT_RDIV_0" |
159 "REAL_LT_NEGTOTAL" > "HOL4Real.real.REAL_LT_NEGTOTAL" |
159 "REAL_LT_NEGTOTAL" > "HOL4Real.real.REAL_LT_NEGTOTAL" |
160 "REAL_LT_NEG" > "OrderedGroup.neg_less_iff_less" |
160 "REAL_LT_NEG" > "OrderedGroup.neg_less_iff_less" |
161 "REAL_LT_MULTIPLE" > "HOL4Real.real.REAL_LT_MULTIPLE" |
161 "REAL_LT_MULTIPLE" > "HOL4Real.real.REAL_LT_MULTIPLE" |
162 "REAL_LT_MUL2" > "Ring_and_Field.mult_strict_mono'" |
162 "REAL_LT_MUL2" > "Ring_and_Field.mult_strict_mono'" |
163 "REAL_LT_MUL" > "Ring_and_Field.mult_pos_pos" |
163 "REAL_LT_MUL" > "Ring_and_Field.mult_pos_pos" |
164 "REAL_LT_LMUL_IMP" > "Ring_and_Field.ordered_comm_semiring_strict_class.mult_strict_mono" |
164 "REAL_LT_LMUL_IMP" > "Ring_and_Field.linordered_comm_semiring_strict_class.mult_strict_mono" |
165 "REAL_LT_LMUL_0" > "HOL4Real.real.REAL_LT_LMUL_0" |
165 "REAL_LT_LMUL_0" > "HOL4Real.real.REAL_LT_LMUL_0" |
166 "REAL_LT_LMUL" > "HOL4Real.real.REAL_LT_LMUL" |
166 "REAL_LT_LMUL" > "HOL4Real.real.REAL_LT_LMUL" |
167 "REAL_LT_LE" > "Orderings.order_class.order_less_le" |
167 "REAL_LT_LE" > "Orderings.order_class.order_less_le" |
168 "REAL_LT_LDIV_EQ" > "Ring_and_Field.pos_divide_less_eq" |
168 "REAL_LT_LDIV_EQ" > "Ring_and_Field.pos_divide_less_eq" |
169 "REAL_LT_LADD" > "OrderedGroup.add_less_cancel_left" |
169 "REAL_LT_LADD" > "OrderedGroup.add_less_cancel_left" |
186 "REAL_LT_ADDL" > "HOL4Real.real.REAL_LT_ADDL" |
186 "REAL_LT_ADDL" > "HOL4Real.real.REAL_LT_ADDL" |
187 "REAL_LT_ADD2" > "OrderedGroup.add_strict_mono" |
187 "REAL_LT_ADD2" > "OrderedGroup.add_strict_mono" |
188 "REAL_LT_ADD1" > "HOL4Real.real.REAL_LT_ADD1" |
188 "REAL_LT_ADD1" > "HOL4Real.real.REAL_LT_ADD1" |
189 "REAL_LT_ADD" > "OrderedGroup.add_pos_pos" |
189 "REAL_LT_ADD" > "OrderedGroup.add_pos_pos" |
190 "REAL_LT_1" > "HOL4Real.real.REAL_LT_1" |
190 "REAL_LT_1" > "HOL4Real.real.REAL_LT_1" |
191 "REAL_LT_01" > "Ring_and_Field.ordered_semidom_class.zero_less_one" |
191 "REAL_LT_01" > "Ring_and_Field.zero_less_one" |
192 "REAL_LTE_TRANS" > "Set.basic_trans_rules_24" |
192 "REAL_LTE_TRANS" > "Set.basic_trans_rules_24" |
193 "REAL_LTE_TOTAL" > "HOL4Real.real.REAL_LTE_TOTAL" |
193 "REAL_LTE_TOTAL" > "HOL4Real.real.REAL_LTE_TOTAL" |
194 "REAL_LTE_ANTSYM" > "HOL4Real.real.REAL_LTE_ANTSYM" |
194 "REAL_LTE_ANTSYM" > "HOL4Real.real.REAL_LTE_ANTSYM" |
195 "REAL_LTE_ADD2" > "OrderedGroup.add_less_le_mono" |
195 "REAL_LTE_ADD2" > "OrderedGroup.add_less_le_mono" |
196 "REAL_LTE_ADD" > "OrderedGroup.add_pos_nonneg" |
196 "REAL_LTE_ADD" > "OrderedGroup.add_pos_nonneg" |
202 "REAL_LE_TOTAL" > "Orderings.linorder_class.linorder_linear" |
202 "REAL_LE_TOTAL" > "Orderings.linorder_class.linorder_linear" |
203 "REAL_LE_SUB_RADD" > "OrderedGroup.compare_rls_8" |
203 "REAL_LE_SUB_RADD" > "OrderedGroup.compare_rls_8" |
204 "REAL_LE_SUB_LADD" > "OrderedGroup.compare_rls_9" |
204 "REAL_LE_SUB_LADD" > "OrderedGroup.compare_rls_9" |
205 "REAL_LE_SQUARE" > "Ring_and_Field.zero_le_square" |
205 "REAL_LE_SQUARE" > "Ring_and_Field.zero_le_square" |
206 "REAL_LE_RNEG" > "OrderedGroup.le_eq_neg" |
206 "REAL_LE_RNEG" > "OrderedGroup.le_eq_neg" |
207 "REAL_LE_RMUL_IMP" > "Ring_and_Field.pordered_semiring_class.mult_right_mono" |
207 "REAL_LE_RMUL_IMP" > "Ring_and_Field.mult_right_mono" |
208 "REAL_LE_RMUL" > "RealDef.real_mult_le_cancel_iff1" |
208 "REAL_LE_RMUL" > "RealDef.real_mult_le_cancel_iff1" |
209 "REAL_LE_REFL" > "Finite_Set.max.f_below.below_refl" |
209 "REAL_LE_REFL" > "Finite_Set.max.f_below.below_refl" |
210 "REAL_LE_RDIV_EQ" > "Ring_and_Field.pos_le_divide_eq" |
210 "REAL_LE_RDIV_EQ" > "Ring_and_Field.pos_le_divide_eq" |
211 "REAL_LE_RDIV" > "Ring_and_Field.mult_imp_le_div_pos" |
211 "REAL_LE_RDIV" > "Ring_and_Field.mult_imp_le_div_pos" |
212 "REAL_LE_RADD" > "OrderedGroup.add_le_cancel_right" |
212 "REAL_LE_RADD" > "OrderedGroup.add_le_cancel_right" |
218 "REAL_LE_NEG" > "OrderedGroup.neg_le_iff_le" |
218 "REAL_LE_NEG" > "OrderedGroup.neg_le_iff_le" |
219 "REAL_LE_MUL2" > "HOL4Real.real.REAL_LE_MUL2" |
219 "REAL_LE_MUL2" > "HOL4Real.real.REAL_LE_MUL2" |
220 "REAL_LE_MUL" > "Ring_and_Field.mult_nonneg_nonneg" |
220 "REAL_LE_MUL" > "Ring_and_Field.mult_nonneg_nonneg" |
221 "REAL_LE_LT" > "Orderings.order_le_less" |
221 "REAL_LE_LT" > "Orderings.order_le_less" |
222 "REAL_LE_LNEG" > "RealDef.real_0_le_add_iff" |
222 "REAL_LE_LNEG" > "RealDef.real_0_le_add_iff" |
223 "REAL_LE_LMUL_IMP" > "Ring_and_Field.pordered_comm_semiring_class.mult_mono" |
223 "REAL_LE_LMUL_IMP" > "Ring_and_Field.mult_mono" |
224 "REAL_LE_LMUL" > "RealDef.real_mult_le_cancel_iff2" |
224 "REAL_LE_LMUL" > "RealDef.real_mult_le_cancel_iff2" |
225 "REAL_LE_LDIV_EQ" > "Ring_and_Field.pos_divide_le_eq" |
225 "REAL_LE_LDIV_EQ" > "Ring_and_Field.pos_divide_le_eq" |
226 "REAL_LE_LDIV" > "Ring_and_Field.mult_imp_div_pos_le" |
226 "REAL_LE_LDIV" > "Ring_and_Field.mult_imp_div_pos_le" |
227 "REAL_LE_LADD_IMP" > "OrderedGroup.pordered_ab_semigroup_add_class.add_left_mono" |
227 "REAL_LE_LADD_IMP" > "OrderedGroup.add_left_mono" |
228 "REAL_LE_LADD" > "OrderedGroup.add_le_cancel_left" |
228 "REAL_LE_LADD" > "OrderedGroup.add_le_cancel_left" |
229 "REAL_LE_INV_EQ" > "Ring_and_Field.inverse_nonnegative_iff_nonnegative" |
229 "REAL_LE_INV_EQ" > "Ring_and_Field.inverse_nonnegative_iff_nonnegative" |
230 "REAL_LE_INV" > "HOL4Real.real.REAL_LE_INV" |
230 "REAL_LE_INV" > "HOL4Real.real.REAL_LE_INV" |
231 "REAL_LE_DOUBLE" > "OrderedGroup.zero_le_double_add_iff_zero_le_single_add" |
231 "REAL_LE_DOUBLE" > "OrderedGroup.zero_le_double_add_iff_zero_le_single_add" |
232 "REAL_LE_DIV" > "HOL4Real.real.REAL_LE_DIV" |
232 "REAL_LE_DIV" > "HOL4Real.real.REAL_LE_DIV" |