89 "TREAL_ADD_LINV" > "HOL4Real.realax.TREAL_ADD_LINV" |
89 "TREAL_ADD_LINV" > "HOL4Real.realax.TREAL_ADD_LINV" |
90 "TREAL_ADD_LID" > "HOL4Real.realax.TREAL_ADD_LID" |
90 "TREAL_ADD_LID" > "HOL4Real.realax.TREAL_ADD_LID" |
91 "TREAL_ADD_ASSOC" > "HOL4Real.realax.TREAL_ADD_ASSOC" |
91 "TREAL_ADD_ASSOC" > "HOL4Real.realax.TREAL_ADD_ASSOC" |
92 "TREAL_10" > "HOL4Real.realax.TREAL_10" |
92 "TREAL_10" > "HOL4Real.realax.TREAL_10" |
93 "REAL_SUP_ALLPOS" > "HOL4Compat.REAL_SUP_ALLPOS" |
93 "REAL_SUP_ALLPOS" > "HOL4Compat.REAL_SUP_ALLPOS" |
94 "REAL_MUL_SYM" > "Ring_and_Field.ring_eq_simps_2" |
94 "REAL_MUL_SYM" > "Ring_and_Field.ring_eq_simps_6" |
95 "REAL_MUL_LINV" > "HOL4Compat.REAL_MUL_LINV" |
95 "REAL_MUL_LINV" > "HOL4Compat.REAL_MUL_LINV" |
96 "REAL_MUL_LID" > "OrderedGroup.comm_monoid_mult.mult_1" |
96 "REAL_MUL_LID" > "OrderedGroup.comm_monoid_mult.mult_1" |
97 "REAL_MUL_ASSOC" > "HOL4Compat.REAL_MUL_ASSOC" |
97 "REAL_MUL_ASSOC" > "HOL4Compat.REAL_MUL_ASSOC" |
98 "REAL_LT_TRANS" > "Set.basic_trans_rules_21" |
98 "REAL_LT_TRANS" > "Set.basic_trans_rules_21" |
99 "REAL_LT_TOTAL" > "HOL4Compat.REAL_LT_TOTAL" |
99 "REAL_LT_TOTAL" > "HOL4Compat.REAL_LT_TOTAL" |
100 "REAL_LT_REFL" > "HOL.order_less_irrefl" |
100 "REAL_LT_REFL" > "Orderings.order_less_irrefl" |
101 "REAL_LT_MUL" > "Ring_and_Field.mult_pos" |
101 "REAL_LT_MUL" > "Ring_and_Field.mult_pos" |
102 "REAL_LT_IADD" > "OrderedGroup.add_strict_left_mono" |
102 "REAL_LT_IADD" > "OrderedGroup.add_strict_left_mono" |
103 "REAL_LDISTRIB" > "Ring_and_Field.ring_eq_simps_5" |
103 "REAL_LDISTRIB" > "Ring_and_Field.ring_eq_simps_2" |
104 "REAL_INV_0" > "Ring_and_Field.division_by_zero.inverse_zero" |
104 "REAL_INV_0" > "Ring_and_Field.division_by_zero.inverse_zero" |
105 "REAL_ADD_SYM" > "Ring_and_Field.ring_eq_simps_9" |
105 "REAL_ADD_SYM" > "Ring_and_Field.ring_eq_simps_9" |
106 "REAL_ADD_LINV" > "HOL4Compat.REAL_ADD_LINV" |
106 "REAL_ADD_LINV" > "HOL4Compat.REAL_ADD_LINV" |
107 "REAL_ADD_LID" > "OrderedGroup.comm_monoid_add.add_0" |
107 "REAL_ADD_LID" > "OrderedGroup.comm_monoid_add.add_0" |
108 "REAL_ADD_ASSOC" > "HOL4Compat.REAL_ADD_ASSOC" |
108 "REAL_ADD_ASSOC" > "HOL4Compat.REAL_ADD_ASSOC" |