author | haftmann |
Mon, 19 Jul 2010 16:09:44 +0200 | |
changeset 37887 | 2ae085b07f2f |
parent 36776 | c137ae7673d3 |
child 44763 | b50d5d694838 |
permissions | -rw-r--r-- |
14516 | 1 |
import |
2 |
||
3 |
import_segment "hol4" |
|
4 |
||
5 |
def_maps |
|
6 |
"sup" > "sup_def" |
|
7 |
"sumc" > "sumc_def" |
|
8 |
"sum" > "sum_def" |
|
9 |
||
10 |
const_maps |
|
11 |
"sup" > "HOL4Real.real.sup" |
|
12 |
"sum" > "HOL4Real.real.sum" |
|
35267
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35092
diff
changeset
|
13 |
"real_sub" > "Groups.minus" :: "real => real => real" |
14516 | 14 |
"real_of_num" > "RealDef.real" :: "nat => real" |
35092
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35085
diff
changeset
|
15 |
"real_lte" > "Orderings.less_eq" :: "real => real => bool" |
14516 | 16 |
"real_gt" > "HOL4Compat.real_gt" |
17 |
"real_ge" > "HOL4Compat.real_ge" |
|
24996 | 18 |
"pow" > "Power.power_class.power" :: "real => nat => real" |
35092
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35085
diff
changeset
|
19 |
"abs" > "Groups.abs" :: "real => real" |
35085 | 20 |
"/" > "Ring.divide" :: "real => real => real" |
14516 | 21 |
|
22 |
thm_maps |
|
23 |
"sup_def" > "HOL4Real.real.sup_def" |
|
24 |
"sup" > "HOL4Real.real.sup" |
|
25 |
"sumc" > "HOL4Real.real.sumc" |
|
26 |
"sum_def" > "HOL4Real.real.sum_def" |
|
27 |
"sum" > "HOL4Real.real.sum" |
|
37887 | 28 |
"real_sub" > "Groups.diff_minus" |
14516 | 29 |
"real_of_num" > "HOL4Compat.real_of_num" |
30 |
"real_lte" > "HOL4Compat.real_lte" |
|
15647 | 31 |
"real_lt" > "Orderings.linorder_not_le" |
14516 | 32 |
"real_gt" > "HOL4Compat.real_gt" |
33 |
"real_ge" > "HOL4Compat.real_ge" |
|
35085 | 34 |
"real_div" > "Ring.divide_inverse" |
14516 | 35 |
"pow" > "HOL4Compat.pow" |
36 |
"abs" > "HOL4Compat.abs" |
|
37 |
"SUP_LEMMA3" > "HOL4Real.real.SUP_LEMMA3" |
|
38 |
"SUP_LEMMA2" > "HOL4Real.real.SUP_LEMMA2" |
|
39 |
"SUP_LEMMA1" > "HOL4Real.real.SUP_LEMMA1" |
|
40 |
"SUM_ZERO" > "HOL4Real.real.SUM_ZERO" |
|
41 |
"SUM_TWO" > "HOL4Real.real.SUM_TWO" |
|
42 |
"SUM_SUBST" > "HOL4Real.real.SUM_SUBST" |
|
43 |
"SUM_SUB" > "HOL4Real.real.SUM_SUB" |
|
44 |
"SUM_REINDEX" > "HOL4Real.real.SUM_REINDEX" |
|
45 |
"SUM_POS_GEN" > "HOL4Real.real.SUM_POS_GEN" |
|
46 |
"SUM_POS" > "HOL4Real.real.SUM_POS" |
|
47 |
"SUM_PERMUTE_0" > "HOL4Real.real.SUM_PERMUTE_0" |
|
48 |
"SUM_OFFSET" > "HOL4Real.real.SUM_OFFSET" |
|
49 |
"SUM_NSUB" > "HOL4Real.real.SUM_NSUB" |
|
50 |
"SUM_NEG" > "HOL4Real.real.SUM_NEG" |
|
51 |
"SUM_LE" > "HOL4Real.real.SUM_LE" |
|
52 |
"SUM_GROUP" > "HOL4Real.real.SUM_GROUP" |
|
53 |
"SUM_EQ" > "HOL4Real.real.SUM_EQ" |
|
54 |
"SUM_DIFF" > "HOL4Real.real.SUM_DIFF" |
|
55 |
"SUM_DEF" > "HOL4Real.real.SUM_DEF" |
|
56 |
"SUM_CMUL" > "HOL4Real.real.SUM_CMUL" |
|
57 |
"SUM_CANCEL" > "HOL4Real.real.SUM_CANCEL" |
|
58 |
"SUM_BOUND" > "HOL4Real.real.SUM_BOUND" |
|
59 |
"SUM_ADD" > "HOL4Real.real.SUM_ADD" |
|
60 |
"SUM_ABS_LE" > "HOL4Real.real.SUM_ABS_LE" |
|
61 |
"SUM_ABS" > "HOL4Real.real.SUM_ABS" |
|
62 |
"SUM_2" > "HOL4Real.real.SUM_2" |
|
63 |
"SUM_1" > "HOL4Real.real.SUM_1" |
|
64 |
"SUM_0" > "HOL4Real.real.SUM_0" |
|
65 |
"SETOK_LE_LT" > "HOL4Real.real.SETOK_LE_LT" |
|
66 |
"REAL_SUP_UBOUND_LE" > "HOL4Real.real.REAL_SUP_UBOUND_LE" |
|
67 |
"REAL_SUP_UBOUND" > "HOL4Real.real.REAL_SUP_UBOUND" |
|
68 |
"REAL_SUP_SOMEPOS" > "HOL4Real.real.REAL_SUP_SOMEPOS" |
|
69 |
"REAL_SUP_LE" > "HOL4Real.real.REAL_SUP_LE" |
|
70 |
"REAL_SUP_EXISTS" > "HOL4Real.real.REAL_SUP_EXISTS" |
|
71 |
"REAL_SUP_ALLPOS" > "HOL4Compat.REAL_SUP_ALLPOS" |
|
72 |
"REAL_SUP" > "HOL4Real.real.REAL_SUP" |
|
73 |
"REAL_SUMSQ" > "HOL4Real.real.REAL_SUMSQ" |
|
74 |
"REAL_SUB_TRIANGLE" > "HOL4Real.real.REAL_SUB_TRIANGLE" |
|
75 |
"REAL_SUB_SUB2" > "HOL4Real.real.REAL_SUB_SUB2" |
|
76 |
"REAL_SUB_SUB" > "HOL4Real.real.REAL_SUB_SUB" |
|
35050
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35028
diff
changeset
|
77 |
"REAL_SUB_RZERO" > "Groups.diff_0_right" |
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35028
diff
changeset
|
78 |
"REAL_SUB_RNEG" > "Groups.diff_minus_eq_add" |
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35028
diff
changeset
|
79 |
"REAL_SUB_REFL" > "Groups.diff_self" |
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35028
diff
changeset
|
80 |
"REAL_SUB_RDISTRIB" > "Rings.ring_eq_simps_3" |
14516 | 81 |
"REAL_SUB_NEG2" > "HOL4Real.real.REAL_SUB_NEG2" |
35050
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35028
diff
changeset
|
82 |
"REAL_SUB_LZERO" > "Groups.diff_0" |
15647 | 83 |
"REAL_SUB_LT" > "HOL4Real.real.REAL_SUB_LT" |
14516 | 84 |
"REAL_SUB_LNEG" > "HOL4Real.real.REAL_SUB_LNEG" |
15647 | 85 |
"REAL_SUB_LE" > "HOL4Real.real.REAL_SUB_LE" |
35050
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35028
diff
changeset
|
86 |
"REAL_SUB_LDISTRIB" > "Rings.ring_eq_simps_4" |
14516 | 87 |
"REAL_SUB_INV2" > "HOL4Real.real.REAL_SUB_INV2" |
14796 | 88 |
"REAL_SUB_ADD2" > "HOL4Real.real.REAL_SUB_ADD2" |
35050
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35028
diff
changeset
|
89 |
"REAL_SUB_ADD" > "Groups.diff_add_cancel" |
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35028
diff
changeset
|
90 |
"REAL_SUB_ABS" > "Groups.abs_triangle_ineq2" |
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35028
diff
changeset
|
91 |
"REAL_SUB_0" > "Groups.diff_eq_0_iff_eq" |
14516 | 92 |
"REAL_RNEG_UNIQ" > "RealDef.real_add_eq_0_iff" |
35050
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35028
diff
changeset
|
93 |
"REAL_RINV_UNIQ" > "Rings.inverse_unique" |
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35028
diff
changeset
|
94 |
"REAL_RDISTRIB" > "Rings.ring_eq_simps_1" |
14516 | 95 |
"REAL_POW_POW" > "Power.power_mult" |
17188 | 96 |
"REAL_POW_MONO_LT" > "HOL4Real.real.REAL_POW_MONO_LT" |
14516 | 97 |
"REAL_POW_LT2" > "HOL4Real.real.REAL_POW_LT2" |
98 |
"REAL_POW_LT" > "Power.zero_less_power" |
|
99 |
"REAL_POW_INV" > "Power.power_inverse" |
|
100 |
"REAL_POW_DIV" > "Power.power_divide" |
|
101 |
"REAL_POW_ADD" > "Power.power_add" |
|
30925 | 102 |
"REAL_POW2_ABS" > "Nat_Numeral.power2_abs" |
14516 | 103 |
"REAL_POS_NZ" > "HOL4Real.real.REAL_POS_NZ" |
104 |
"REAL_POS" > "RealDef.real_of_nat_ge_zero" |
|
105 |
"REAL_POASQ" > "HOL4Real.real.REAL_POASQ" |
|
35050
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35028
diff
changeset
|
106 |
"REAL_OVER1" > "Rings.divide_1" |
14516 | 107 |
"REAL_OF_NUM_SUC" > "RealDef.real_of_nat_Suc" |
35344
e0b46cd72414
moved some lemmas from RealPow to RealDef; changed orientation of real_of_int_power
huffman
parents:
35267
diff
changeset
|
108 |
"REAL_OF_NUM_POW" > "RealDef.power_real_of_nat" |
14516 | 109 |
"REAL_OF_NUM_MUL" > "RealDef.real_of_nat_mult" |
110 |
"REAL_OF_NUM_LE" > "RealDef.real_of_nat_le_iff" |
|
111 |
"REAL_OF_NUM_EQ" > "RealDef.real_of_nat_inject" |
|
112 |
"REAL_OF_NUM_ADD" > "RealDef.real_of_nat_add" |
|
113 |
"REAL_NZ_IMP_LT" > "HOL4Real.real.REAL_NZ_IMP_LT" |
|
114 |
"REAL_NOT_LT" > "HOL4Compat.real_lte" |
|
15647 | 115 |
"REAL_NOT_LE" > "Orderings.linorder_not_le" |
35050
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35028
diff
changeset
|
116 |
"REAL_NEG_SUB" > "Groups.minus_diff_eq" |
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35028
diff
changeset
|
117 |
"REAL_NEG_RMUL" > "Rings.mult_minus_right" |
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35028
diff
changeset
|
118 |
"REAL_NEG_NEG" > "Groups.minus_minus" |
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35028
diff
changeset
|
119 |
"REAL_NEG_MUL2" > "Rings.minus_mult_minus" |
14516 | 120 |
"REAL_NEG_MINUS1" > "HOL4Real.real.REAL_NEG_MINUS1" |
35050
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35028
diff
changeset
|
121 |
"REAL_NEG_LT0" > "Groups.neg_less_0_iff_less" |
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35028
diff
changeset
|
122 |
"REAL_NEG_LMUL" > "Rings.mult_minus_left" |
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35028
diff
changeset
|
123 |
"REAL_NEG_LE0" > "Groups.neg_le_0_iff_le" |
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35028
diff
changeset
|
124 |
"REAL_NEG_INV" > "Rings.nonzero_inverse_minus_eq" |
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35028
diff
changeset
|
125 |
"REAL_NEG_GT0" > "Groups.neg_0_less_iff_less" |
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35028
diff
changeset
|
126 |
"REAL_NEG_GE0" > "Groups.neg_0_le_iff_le" |
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35028
diff
changeset
|
127 |
"REAL_NEG_EQ0" > "Groups.neg_equal_0_iff_equal" |
14516 | 128 |
"REAL_NEG_EQ" > "HOL4Real.real.REAL_NEG_EQ" |
35050
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35028
diff
changeset
|
129 |
"REAL_NEG_ADD" > "Groups.minus_add_distrib" |
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35028
diff
changeset
|
130 |
"REAL_NEG_0" > "Groups.minus_zero" |
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35028
diff
changeset
|
131 |
"REAL_NEGNEG" > "Groups.minus_minus" |
25930 | 132 |
"REAL_MUL_SYM" > "Int.zmult_ac_2" |
35050
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35028
diff
changeset
|
133 |
"REAL_MUL_RZERO" > "Rings.mult_zero_right" |
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35028
diff
changeset
|
134 |
"REAL_MUL_RNEG" > "Rings.mult_minus_right" |
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35028
diff
changeset
|
135 |
"REAL_MUL_RINV" > "Rings.right_inverse" |
17188 | 136 |
"REAL_MUL_RID" > "Finite_Set.AC_mult.f_e.ident" |
35050
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35028
diff
changeset
|
137 |
"REAL_MUL_LZERO" > "Rings.mult_zero_left" |
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35028
diff
changeset
|
138 |
"REAL_MUL_LNEG" > "Rings.mult_minus_left" |
14516 | 139 |
"REAL_MUL_LINV" > "HOL4Compat.REAL_MUL_LINV" |
17188 | 140 |
"REAL_MUL_LID" > "Finite_Set.AC_mult.f_e.left_ident" |
14516 | 141 |
"REAL_MUL_ASSOC" > "HOL4Compat.REAL_MUL_ASSOC" |
142 |
"REAL_MUL" > "RealDef.real_of_nat_mult" |
|
143 |
"REAL_MIDDLE2" > "HOL4Real.real.REAL_MIDDLE2" |
|
144 |
"REAL_MIDDLE1" > "HOL4Real.real.REAL_MIDDLE1" |
|
35050
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35028
diff
changeset
|
145 |
"REAL_MEAN" > "Rings.dense" |
14516 | 146 |
"REAL_LT_TRANS" > "Set.basic_trans_rules_21" |
147 |
"REAL_LT_TOTAL" > "HOL4Compat.REAL_LT_TOTAL" |
|
35050
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35028
diff
changeset
|
148 |
"REAL_LT_SUB_RADD" > "Groups.compare_rls_6" |
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35028
diff
changeset
|
149 |
"REAL_LT_SUB_LADD" > "Groups.compare_rls_7" |
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35028
diff
changeset
|
150 |
"REAL_LT_RMUL_IMP" > "Rings.mult_strict_right_mono" |
14516 | 151 |
"REAL_LT_RMUL_0" > "HOL4Real.real.REAL_LT_RMUL_0" |
152 |
"REAL_LT_RMUL" > "RealDef.real_mult_less_iff1" |
|
15647 | 153 |
"REAL_LT_REFL" > "Orderings.order_less_irrefl" |
35050
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35028
diff
changeset
|
154 |
"REAL_LT_RDIV_EQ" > "Rings.pos_less_divide_eq" |
14516 | 155 |
"REAL_LT_RDIV_0" > "HOL4Real.real.REAL_LT_RDIV_0" |
156 |
"REAL_LT_RDIV" > "HOL4Real.real.REAL_LT_RDIV" |
|
35050
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35028
diff
changeset
|
157 |
"REAL_LT_RADD" > "Groups.add_less_cancel_right" |
14516 | 158 |
"REAL_LT_NZ" > "HOL4Real.real.REAL_LT_NZ" |
159 |
"REAL_LT_NEGTOTAL" > "HOL4Real.real.REAL_LT_NEGTOTAL" |
|
35050
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35028
diff
changeset
|
160 |
"REAL_LT_NEG" > "Groups.neg_less_iff_less" |
14516 | 161 |
"REAL_LT_MULTIPLE" > "HOL4Real.real.REAL_LT_MULTIPLE" |
35050
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35028
diff
changeset
|
162 |
"REAL_LT_MUL2" > "Rings.mult_strict_mono'" |
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35028
diff
changeset
|
163 |
"REAL_LT_MUL" > "Rings.mult_pos_pos" |
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35028
diff
changeset
|
164 |
"REAL_LT_LMUL_IMP" > "Rings.linordered_comm_semiring_strict_class.mult_strict_mono" |
14516 | 165 |
"REAL_LT_LMUL_0" > "HOL4Real.real.REAL_LT_LMUL_0" |
166 |
"REAL_LT_LMUL" > "HOL4Real.real.REAL_LT_LMUL" |
|
17644 | 167 |
"REAL_LT_LE" > "Orderings.order_class.order_less_le" |
35050
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35028
diff
changeset
|
168 |
"REAL_LT_LDIV_EQ" > "Rings.pos_divide_less_eq" |
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35028
diff
changeset
|
169 |
"REAL_LT_LADD" > "Groups.add_less_cancel_left" |
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35028
diff
changeset
|
170 |
"REAL_LT_INV_EQ" > "Rings.inverse_positive_iff_positive" |
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35028
diff
changeset
|
171 |
"REAL_LT_INV" > "Rings.less_imp_inverse_less" |
15647 | 172 |
"REAL_LT_IMP_NE" > "Orderings.less_imp_neq" |
173 |
"REAL_LT_IMP_LE" > "Orderings.order_less_imp_le" |
|
35050
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35028
diff
changeset
|
174 |
"REAL_LT_IADD" > "Groups.add_strict_left_mono" |
14516 | 175 |
"REAL_LT_HALF2" > "HOL4Real.real.REAL_LT_HALF2" |
176 |
"REAL_LT_HALF1" > "NatSimprocs.half_gt_zero_iff" |
|
15647 | 177 |
"REAL_LT_GT" > "Orderings.order_less_not_sym" |
14516 | 178 |
"REAL_LT_FRACTION_0" > "HOL4Real.real.REAL_LT_FRACTION_0" |
179 |
"REAL_LT_FRACTION" > "HOL4Real.real.REAL_LT_FRACTION" |
|
35050
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35028
diff
changeset
|
180 |
"REAL_LT_DIV" > "Rings.divide_pos_pos" |
14516 | 181 |
"REAL_LT_ANTISYM" > "HOL4Real.real.REAL_LT_ANTISYM" |
35050
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35028
diff
changeset
|
182 |
"REAL_LT_ADD_SUB" > "Groups.compare_rls_7" |
14516 | 183 |
"REAL_LT_ADDR" > "HOL4Real.real.REAL_LT_ADDR" |
184 |
"REAL_LT_ADDNEG2" > "HOL4Real.real.REAL_LT_ADDNEG2" |
|
185 |
"REAL_LT_ADDNEG" > "HOL4Real.real.REAL_LT_ADDNEG" |
|
186 |
"REAL_LT_ADDL" > "HOL4Real.real.REAL_LT_ADDL" |
|
35050
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35028
diff
changeset
|
187 |
"REAL_LT_ADD2" > "Groups.add_strict_mono" |
14516 | 188 |
"REAL_LT_ADD1" > "HOL4Real.real.REAL_LT_ADD1" |
35050
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35028
diff
changeset
|
189 |
"REAL_LT_ADD" > "Groups.add_pos_pos" |
14516 | 190 |
"REAL_LT_1" > "HOL4Real.real.REAL_LT_1" |
35050
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35028
diff
changeset
|
191 |
"REAL_LT_01" > "Rings.zero_less_one" |
14516 | 192 |
"REAL_LTE_TRANS" > "Set.basic_trans_rules_24" |
193 |
"REAL_LTE_TOTAL" > "HOL4Real.real.REAL_LTE_TOTAL" |
|
194 |
"REAL_LTE_ANTSYM" > "HOL4Real.real.REAL_LTE_ANTSYM" |
|
35050
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35028
diff
changeset
|
195 |
"REAL_LTE_ADD2" > "Groups.add_less_le_mono" |
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35028
diff
changeset
|
196 |
"REAL_LTE_ADD" > "Groups.add_pos_nonneg" |
14516 | 197 |
"REAL_LT1_POW2" > "HOL4Real.real.REAL_LT1_POW2" |
198 |
"REAL_LT" > "RealDef.real_of_nat_less_iff" |
|
199 |
"REAL_LNEG_UNIQ" > "HOL4Real.real.REAL_LNEG_UNIQ" |
|
200 |
"REAL_LINV_UNIQ" > "HOL4Real.real.REAL_LINV_UNIQ" |
|
201 |
"REAL_LE_TRANS" > "Set.basic_trans_rules_25" |
|
17644 | 202 |
"REAL_LE_TOTAL" > "Orderings.linorder_class.linorder_linear" |
35050
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35028
diff
changeset
|
203 |
"REAL_LE_SUB_RADD" > "Groups.compare_rls_8" |
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35028
diff
changeset
|
204 |
"REAL_LE_SUB_LADD" > "Groups.compare_rls_9" |
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35028
diff
changeset
|
205 |
"REAL_LE_SQUARE" > "Rings.zero_le_square" |
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35028
diff
changeset
|
206 |
"REAL_LE_RNEG" > "Groups.le_eq_neg" |
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35028
diff
changeset
|
207 |
"REAL_LE_RMUL_IMP" > "Rings.mult_right_mono" |
14516 | 208 |
"REAL_LE_RMUL" > "RealDef.real_mult_le_cancel_iff1" |
17188 | 209 |
"REAL_LE_REFL" > "Finite_Set.max.f_below.below_refl" |
35050
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35028
diff
changeset
|
210 |
"REAL_LE_RDIV_EQ" > "Rings.pos_le_divide_eq" |
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35028
diff
changeset
|
211 |
"REAL_LE_RDIV" > "Rings.mult_imp_le_div_pos" |
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35028
diff
changeset
|
212 |
"REAL_LE_RADD" > "Groups.add_le_cancel_right" |
30925 | 213 |
"REAL_LE_POW2" > "Nat_Numeral.zero_compare_simps_12" |
14516 | 214 |
"REAL_LE_NEGTOTAL" > "HOL4Real.real.REAL_LE_NEGTOTAL" |
35050
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35028
diff
changeset
|
215 |
"REAL_LE_NEGR" > "Groups.le_minus_self_iff" |
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35028
diff
changeset
|
216 |
"REAL_LE_NEGL" > "Groups.minus_le_self_iff" |
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35028
diff
changeset
|
217 |
"REAL_LE_NEG2" > "Groups.neg_le_iff_le" |
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35028
diff
changeset
|
218 |
"REAL_LE_NEG" > "Groups.neg_le_iff_le" |
14516 | 219 |
"REAL_LE_MUL2" > "HOL4Real.real.REAL_LE_MUL2" |
35050
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35028
diff
changeset
|
220 |
"REAL_LE_MUL" > "Rings.mult_nonneg_nonneg" |
15647 | 221 |
"REAL_LE_LT" > "Orderings.order_le_less" |
14516 | 222 |
"REAL_LE_LNEG" > "RealDef.real_0_le_add_iff" |
35050
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35028
diff
changeset
|
223 |
"REAL_LE_LMUL_IMP" > "Rings.mult_mono" |
14516 | 224 |
"REAL_LE_LMUL" > "RealDef.real_mult_le_cancel_iff2" |
35050
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35028
diff
changeset
|
225 |
"REAL_LE_LDIV_EQ" > "Rings.pos_divide_le_eq" |
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35028
diff
changeset
|
226 |
"REAL_LE_LDIV" > "Rings.mult_imp_div_pos_le" |
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35028
diff
changeset
|
227 |
"REAL_LE_LADD_IMP" > "Groups.add_left_mono" |
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35028
diff
changeset
|
228 |
"REAL_LE_LADD" > "Groups.add_le_cancel_left" |
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35028
diff
changeset
|
229 |
"REAL_LE_INV_EQ" > "Rings.inverse_nonnegative_iff_nonnegative" |
14516 | 230 |
"REAL_LE_INV" > "HOL4Real.real.REAL_LE_INV" |
35050
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35028
diff
changeset
|
231 |
"REAL_LE_DOUBLE" > "Groups.zero_le_double_add_iff_zero_le_single_add" |
14516 | 232 |
"REAL_LE_DIV" > "HOL4Real.real.REAL_LE_DIV" |
15647 | 233 |
"REAL_LE_ANTISYM" > "Orderings.order_eq_iff" |
14516 | 234 |
"REAL_LE_ADDR" > "HOL4Real.real.REAL_LE_ADDR" |
235 |
"REAL_LE_ADDL" > "HOL4Real.real.REAL_LE_ADDL" |
|
35050
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35028
diff
changeset
|
236 |
"REAL_LE_ADD2" > "Groups.add_mono" |
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35028
diff
changeset
|
237 |
"REAL_LE_ADD" > "Groups.add_nonneg_nonneg" |
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35028
diff
changeset
|
238 |
"REAL_LE_01" > "Rings.zero_le_one" |
14516 | 239 |
"REAL_LET_TRANS" > "Set.basic_trans_rules_23" |
15647 | 240 |
"REAL_LET_TOTAL" > "Orderings.linorder_le_less_linear" |
14516 | 241 |
"REAL_LET_ANTISYM" > "HOL4Real.real.REAL_LET_ANTISYM" |
35050
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35028
diff
changeset
|
242 |
"REAL_LET_ADD2" > "Groups.add_le_less_mono" |
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35028
diff
changeset
|
243 |
"REAL_LET_ADD" > "Groups.add_nonneg_pos" |
14516 | 244 |
"REAL_LE1_POW2" > "HOL4Real.real.REAL_LE1_POW2" |
245 |
"REAL_LE" > "RealDef.real_of_nat_le_iff" |
|
35050
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35028
diff
changeset
|
246 |
"REAL_LDISTRIB" > "Rings.ring_eq_simps_2" |
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35028
diff
changeset
|
247 |
"REAL_INV_POS" > "Rings.positive_imp_inverse_positive" |
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35028
diff
changeset
|
248 |
"REAL_INV_NZ" > "Rings.nonzero_imp_inverse_nonzero" |
14516 | 249 |
"REAL_INV_MUL" > "HOL4Real.real.REAL_INV_MUL" |
36776
c137ae7673d3
remove a couple of redundant lemmas; simplify some proofs
huffman
parents:
36349
diff
changeset
|
250 |
"REAL_INV_LT1" > "Fields.one_less_inverse" |
35050
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35028
diff
changeset
|
251 |
"REAL_INV_INV" > "Rings.inverse_inverse_eq" |
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35028
diff
changeset
|
252 |
"REAL_INV_EQ_0" > "Rings.inverse_nonzero_iff_nonzero" |
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35028
diff
changeset
|
253 |
"REAL_INV_1OVER" > "Rings.inverse_eq_divide" |
36349 | 254 |
"REAL_INV_0" > "Rings.division_ring_inverse_zero_class.inverse_zero" |
35050
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35028
diff
changeset
|
255 |
"REAL_INVINV" > "Rings.nonzero_inverse_inverse_eq" |
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35028
diff
changeset
|
256 |
"REAL_INV1" > "Rings.inverse_1" |
14516 | 257 |
"REAL_INJ" > "RealDef.real_of_nat_inject" |
258 |
"REAL_HALF_DOUBLE" > "RComplete.real_sum_of_halves" |
|
259 |
"REAL_FACT_NZ" > "HOL4Real.real.REAL_FACT_NZ" |
|
35050
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35028
diff
changeset
|
260 |
"REAL_EQ_SUB_RADD" > "Rings.ring_eq_simps_15" |
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35028
diff
changeset
|
261 |
"REAL_EQ_SUB_LADD" > "Rings.ring_eq_simps_16" |
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35028
diff
changeset
|
262 |
"REAL_EQ_RMUL_IMP" > "Rings.field_mult_cancel_right_lemma" |
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35028
diff
changeset
|
263 |
"REAL_EQ_RMUL" > "Rings.field_mult_cancel_right" |
14516 | 264 |
"REAL_EQ_RDIV_EQ" > "HOL4Real.real.REAL_EQ_RDIV_EQ" |
35050
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35028
diff
changeset
|
265 |
"REAL_EQ_RADD" > "Groups.add_right_cancel" |
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35028
diff
changeset
|
266 |
"REAL_EQ_NEG" > "Groups.neg_equal_iff_equal" |
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35028
diff
changeset
|
267 |
"REAL_EQ_MUL_LCANCEL" > "Rings.field_mult_cancel_left" |
14516 | 268 |
"REAL_EQ_LMUL_IMP" > "HOL4Real.real.REAL_EQ_LMUL_IMP" |
269 |
"REAL_EQ_LMUL2" > "RealDef.real_mult_left_cancel" |
|
35050
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35028
diff
changeset
|
270 |
"REAL_EQ_LMUL" > "Rings.field_mult_cancel_left" |
14516 | 271 |
"REAL_EQ_LDIV_EQ" > "HOL4Real.real.REAL_EQ_LDIV_EQ" |
35050
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35028
diff
changeset
|
272 |
"REAL_EQ_LADD" > "Groups.add_left_cancel" |
15647 | 273 |
"REAL_EQ_IMP_LE" > "Orderings.order_eq_refl" |
35050
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35028
diff
changeset
|
274 |
"REAL_ENTIRE" > "Rings.field_mult_eq_0_iff" |
14516 | 275 |
"REAL_DOWN2" > "RealDef.real_lbound_gt_zero" |
276 |
"REAL_DOWN" > "HOL4Real.real.REAL_DOWN" |
|
25930 | 277 |
"REAL_DOUBLE" > "Int.mult_2" |
14516 | 278 |
"REAL_DIV_RMUL" > "HOL4Real.real.REAL_DIV_RMUL" |
35050
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35028
diff
changeset
|
279 |
"REAL_DIV_REFL" > "Rings.divide_self" |
17188 | 280 |
"REAL_DIV_MUL2" > "HOL4Real.real.REAL_DIV_MUL2" |
35050
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35028
diff
changeset
|
281 |
"REAL_DIV_LZERO" > "Rings.divide_zero_left" |
14516 | 282 |
"REAL_DIV_LMUL" > "HOL4Real.real.REAL_DIV_LMUL" |
283 |
"REAL_DIFFSQ" > "HOL4Real.real.REAL_DIFFSQ" |
|
284 |
"REAL_ARCH_LEAST" > "HOL4Real.real.REAL_ARCH_LEAST" |
|
285 |
"REAL_ARCH" > "RComplete.reals_Archimedean3" |
|
17188 | 286 |
"REAL_ADD_SYM" > "Finite_Set.AC_add.f.AC_2" |
14516 | 287 |
"REAL_ADD_SUB2" > "HOL4Real.real.REAL_ADD_SUB2" |
14796 | 288 |
"REAL_ADD_SUB" > "HOL4Real.real.REAL_ADD_SUB" |
35050
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35028
diff
changeset
|
289 |
"REAL_ADD_RINV" > "Groups.right_minus" |
14516 | 290 |
"REAL_ADD_RID_UNIQ" > "HOL4Real.real.REAL_ADD_RID_UNIQ" |
17188 | 291 |
"REAL_ADD_RID" > "Finite_Set.AC_add.f_e.ident" |
35050
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35028
diff
changeset
|
292 |
"REAL_ADD_RDISTRIB" > "Rings.ring_eq_simps_1" |
14516 | 293 |
"REAL_ADD_LINV" > "HOL4Compat.REAL_ADD_LINV" |
294 |
"REAL_ADD_LID_UNIQ" > "HOL4Real.real.REAL_ADD_LID_UNIQ" |
|
17188 | 295 |
"REAL_ADD_LID" > "Finite_Set.AC_add.f_e.left_ident" |
35050
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35028
diff
changeset
|
296 |
"REAL_ADD_LDISTRIB" > "Rings.ring_eq_simps_2" |
14516 | 297 |
"REAL_ADD_ASSOC" > "HOL4Compat.REAL_ADD_ASSOC" |
298 |
"REAL_ADD2_SUB2" > "HOL4Real.real.REAL_ADD2_SUB2" |
|
299 |
"REAL_ADD" > "RealDef.real_of_nat_add" |
|
35050
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35028
diff
changeset
|
300 |
"REAL_ABS_TRIANGLE" > "Groups.abs_triangle_ineq" |
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35028
diff
changeset
|
301 |
"REAL_ABS_POS" > "Groups.abs_ge_zero" |
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35028
diff
changeset
|
302 |
"REAL_ABS_MUL" > "Rings.abs_mult" |
25930 | 303 |
"REAL_ABS_0" > "Int.bin_arith_simps_28" |
14516 | 304 |
"REAL_10" > "HOL4Compat.REAL_10" |
305 |
"REAL_1" > "HOL4Real.real.REAL_1" |
|
306 |
"REAL_0" > "HOL4Real.real.REAL_0" |
|
307 |
"REAL" > "RealDef.real_of_nat_Suc" |
|
308 |
"POW_ZERO_EQ" > "HOL4Real.real.POW_ZERO_EQ" |
|
309 |
"POW_ZERO" > "RealPow.realpow_zero_zero" |
|
310 |
"POW_POS_LT" > "HOL4Real.real.POW_POS_LT" |
|
311 |
"POW_POS" > "Power.zero_le_power" |
|
312 |
"POW_PLUS1" > "HOL4Real.real.POW_PLUS1" |
|
313 |
"POW_ONE" > "Power.power_one" |
|
314 |
"POW_NZ" > "Power.field_power_not_zero" |
|
315 |
"POW_MUL" > "Power.power_mult_distrib" |
|
30925 | 316 |
"POW_MINUS1" > "Nat_Numeral.power_minus1_even" |
14516 | 317 |
"POW_M1" > "HOL4Real.real.POW_M1" |
318 |
"POW_LT" > "HOL4Real.real.POW_LT" |
|
319 |
"POW_LE" > "Power.power_mono" |
|
320 |
"POW_INV" > "Power.nonzero_power_inverse" |
|
321 |
"POW_EQ" > "Power.power_inject_base" |
|
322 |
"POW_ADD" > "Power.power_add" |
|
323 |
"POW_ABS" > "Power.power_abs" |
|
324 |
"POW_2_LT" > "RealPow.two_realpow_gt" |
|
325 |
"POW_2_LE1" > "RealPow.two_realpow_ge_one" |
|
30925 | 326 |
"POW_2" > "Nat_Numeral.power2_eq_square" |
14516 | 327 |
"POW_1" > "Power.power_one_right" |
328 |
"POW_0" > "Power.power_0_Suc" |
|
35050
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35028
diff
changeset
|
329 |
"ABS_ZERO" > "Groups.abs_eq_0" |
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35028
diff
changeset
|
330 |
"ABS_TRIANGLE" > "Groups.abs_triangle_ineq" |
14516 | 331 |
"ABS_SUM" > "HOL4Real.real.ABS_SUM" |
35050
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35028
diff
changeset
|
332 |
"ABS_SUB_ABS" > "Groups.abs_triangle_ineq3" |
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35028
diff
changeset
|
333 |
"ABS_SUB" > "Groups.abs_minus_commute" |
14516 | 334 |
"ABS_STILLNZ" > "HOL4Real.real.ABS_STILLNZ" |
335 |
"ABS_SIGN2" > "HOL4Real.real.ABS_SIGN2" |
|
336 |
"ABS_SIGN" > "HOL4Real.real.ABS_SIGN" |
|
337 |
"ABS_REFL" > "HOL4Real.real.ABS_REFL" |
|
30925 | 338 |
"ABS_POW2" > "Nat_Numeral.abs_power2" |
35050
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35028
diff
changeset
|
339 |
"ABS_POS" > "Groups.abs_ge_zero" |
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35028
diff
changeset
|
340 |
"ABS_NZ" > "Groups.zero_less_abs_iff" |
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35028
diff
changeset
|
341 |
"ABS_NEG" > "Groups.abs_minus_cancel" |
14516 | 342 |
"ABS_N" > "RealDef.abs_real_of_nat_cancel" |
35050
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35028
diff
changeset
|
343 |
"ABS_MUL" > "Rings.abs_mult" |
14516 | 344 |
"ABS_LT_MUL2" > "HOL4Real.real.ABS_LT_MUL2" |
35050
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35028
diff
changeset
|
345 |
"ABS_LE" > "Groups.abs_ge_self" |
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35028
diff
changeset
|
346 |
"ABS_INV" > "Rings.nonzero_abs_inverse" |
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35028
diff
changeset
|
347 |
"ABS_DIV" > "Rings.nonzero_abs_divide" |
14516 | 348 |
"ABS_CIRCLE" > "HOL4Real.real.ABS_CIRCLE" |
349 |
"ABS_CASES" > "HOL4Real.real.ABS_CASES" |
|
350 |
"ABS_BOUNDS" > "RealDef.abs_le_interval_iff" |
|
351 |
"ABS_BOUND" > "HOL4Real.real.ABS_BOUND" |
|
352 |
"ABS_BETWEEN2" > "HOL4Real.real.ABS_BETWEEN2" |
|
353 |
"ABS_BETWEEN1" > "HOL4Real.real.ABS_BETWEEN1" |
|
354 |
"ABS_BETWEEN" > "HOL4Real.real.ABS_BETWEEN" |
|
35050
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35028
diff
changeset
|
355 |
"ABS_ABS" > "Groups.abs_idempotent" |
25930 | 356 |
"ABS_1" > "Int.bin_arith_simps_29" |
357 |
"ABS_0" > "Int.bin_arith_simps_28" |
|
14516 | 358 |
|
359 |
end |