25 "treal_inv" > "HOL4Real.realax.treal_inv" |
25 "treal_inv" > "HOL4Real.realax.treal_inv" |
26 "treal_eq" > "HOL4Real.realax.treal_eq" |
26 "treal_eq" > "HOL4Real.realax.treal_eq" |
27 "treal_add" > "HOL4Real.realax.treal_add" |
27 "treal_add" > "HOL4Real.realax.treal_add" |
28 "treal_1" > "HOL4Real.realax.treal_1" |
28 "treal_1" > "HOL4Real.realax.treal_1" |
29 "treal_0" > "HOL4Real.realax.treal_0" |
29 "treal_0" > "HOL4Real.realax.treal_0" |
30 "real_neg" > "Groups.uminus" :: "real => real" |
30 "real_sub" > "Groups.minus_class.minus" :: "real => real => real" |
31 "real_mul" > "Groups.times" :: "real => real => real" |
31 "real_neg" > "Groups.uminus_class.uminus" :: "real => real" |
32 "real_lt" > "Orderings.less" :: "real => real => bool" |
32 "real_mul" > "Groups.times_class.times" :: "real => real => real" |
33 "real_add" > "Groups.plus" :: "real => real => real" |
33 "real_lt" > "Orderings.ord_class.less" :: "real => real => bool" |
34 "real_1" > "Groups.one" :: "real" |
34 "real_div" > "Fields.inverse_class.divide" :: "real => real => real" |
35 "real_0" > "Groups.zero" :: "real" |
35 "real_add" > "Groups.plus_class.plus" :: "real => real => real" |
36 "inv" > "Ring.inverse" :: "real => real" |
36 "real_1" > "Groups.one_class.one" :: "real" |
|
37 "real_0" > "Groups.zero_class.zero" :: "real" |
|
38 "mk_real" > "HOL.undefined" |
|
39 "inv" > "Fields.inverse_class.inverse" :: "real => real" |
37 "hreal_of_treal" > "HOL4Real.realax.hreal_of_treal" |
40 "hreal_of_treal" > "HOL4Real.realax.hreal_of_treal" |
|
41 "dest_real" > "HOL.undefined" |
38 |
42 |
39 thm_maps |
43 thm_maps |
40 "treal_of_hreal_def" > "HOL4Real.realax.treal_of_hreal_def" |
44 "treal_of_hreal_def" > "HOL4Real.realax.treal_of_hreal_def" |
41 "treal_of_hreal" > "HOL4Real.realax.treal_of_hreal" |
45 "treal_of_hreal" > "HOL4Real.realax.treal_of_hreal" |
42 "treal_neg_def" > "HOL4Real.realax.treal_neg_def" |
46 "treal_neg_def" > "HOL4Real.realax.treal_neg_def" |
89 "TREAL_ADD_LINV" > "HOL4Real.realax.TREAL_ADD_LINV" |
93 "TREAL_ADD_LINV" > "HOL4Real.realax.TREAL_ADD_LINV" |
90 "TREAL_ADD_LID" > "HOL4Real.realax.TREAL_ADD_LID" |
94 "TREAL_ADD_LID" > "HOL4Real.realax.TREAL_ADD_LID" |
91 "TREAL_ADD_ASSOC" > "HOL4Real.realax.TREAL_ADD_ASSOC" |
95 "TREAL_ADD_ASSOC" > "HOL4Real.realax.TREAL_ADD_ASSOC" |
92 "TREAL_10" > "HOL4Real.realax.TREAL_10" |
96 "TREAL_10" > "HOL4Real.realax.TREAL_10" |
93 "REAL_SUP_ALLPOS" > "HOL4Compat.REAL_SUP_ALLPOS" |
97 "REAL_SUP_ALLPOS" > "HOL4Compat.REAL_SUP_ALLPOS" |
94 "REAL_MUL_SYM" > "Int.zmult_ac_2" |
98 "REAL_MUL_SYM" > "Fields.linordered_field_class.sign_simps_21" |
95 "REAL_MUL_LINV" > "HOL4Compat.REAL_MUL_LINV" |
99 "REAL_MUL_LINV" > "Fields.division_ring_class.left_inverse" |
96 "REAL_MUL_LID" > "Finite_Set.AC_mult.f_e.left_ident" |
100 "REAL_MUL_LID" > "Divides.arithmetic_simps_42" |
97 "REAL_MUL_ASSOC" > "HOL4Compat.REAL_MUL_ASSOC" |
101 "REAL_MUL_ASSOC" > "Fields.linordered_field_class.sign_simps_22" |
98 "REAL_LT_TRANS" > "Set.basic_trans_rules_21" |
102 "REAL_LT_TRANS" > "Orderings.order_less_trans" |
99 "REAL_LT_TOTAL" > "HOL4Compat.REAL_LT_TOTAL" |
103 "REAL_LT_TOTAL" > "HOL4Compat.REAL_LT_TOTAL" |
100 "REAL_LT_REFL" > "Orderings.order_less_irrefl" |
104 "REAL_LT_REFL" > "Orderings.order_less_irrefl" |
101 "REAL_LT_MUL" > "Rings.mult_pos_pos" |
105 "REAL_LT_MUL" > "RealDef.real_mult_order" |
102 "REAL_LT_IADD" > "Groups.add_strict_left_mono" |
106 "REAL_LT_IADD" > "Groups.ordered_cancel_ab_semigroup_add_class.add_strict_left_mono" |
103 "REAL_LDISTRIB" > "Rings.ring_eq_simps_2" |
107 "REAL_LDISTRIB" > "Fields.linordered_field_class.sign_simps_7" |
104 "REAL_INV_0" > "Rings.division_ring_inverse_zero_class.inverse_zero" |
108 "REAL_INV_0" > "Fields.division_ring_inverse_zero_class.inverse_zero" |
105 "REAL_ADD_SYM" > "Finite_Set.AC_add.f.AC_2" |
109 "REAL_ADD_SYM" > "Fields.linordered_field_class.sign_simps_18" |
106 "REAL_ADD_LINV" > "HOL4Compat.REAL_ADD_LINV" |
110 "REAL_ADD_LINV" > "Groups.ab_group_add_class.ab_left_minus" |
107 "REAL_ADD_LID" > "Finite_Set.AC_add.f_e.left_ident" |
111 "REAL_ADD_LID" > "Divides.arithmetic_simps_38" |
108 "REAL_ADD_ASSOC" > "HOL4Compat.REAL_ADD_ASSOC" |
112 "REAL_ADD_ASSOC" > "Fields.linordered_field_class.sign_simps_19" |
109 "REAL_10" > "HOL4Compat.REAL_10" |
113 "REAL_10" > "HOL4Compat.REAL_10" |
110 "HREAL_RDISTRIB" > "HOL4Real.realax.HREAL_RDISTRIB" |
114 "HREAL_RDISTRIB" > "HOL4Real.realax.HREAL_RDISTRIB" |
111 "HREAL_LT_REFL" > "HOL4Real.realax.HREAL_LT_REFL" |
115 "HREAL_LT_REFL" > "HOL4Real.realax.HREAL_LT_REFL" |
112 "HREAL_LT_NE" > "HOL4Real.realax.HREAL_LT_NE" |
116 "HREAL_LT_NE" > "HOL4Real.realax.HREAL_LT_NE" |
113 "HREAL_LT_LADD" > "HOL4Real.realax.HREAL_LT_LADD" |
117 "HREAL_LT_LADD" > "HOL4Real.realax.HREAL_LT_LADD" |