author wenzelm Fri May 21 21:42:05 2004 +0200 (2004-05-21) changeset 14796 1e83aa391ade parent 14795 b702848de41f child 14797 546365fe8349
updated;
 src/HOL/Import/HOL/HOL4Real.thy file | annotate | diff | revisions src/HOL/Import/HOL/arithmetic.imp file | annotate | diff | revisions src/HOL/Import/HOL/real.imp file | annotate | diff | revisions src/HOL/Import/HOL/realax.imp file | annotate | diff | revisions
```     1.1 --- a/src/HOL/Import/HOL/HOL4Real.thy	Fri May 21 21:28:58 2004 +0200
1.2 +++ b/src/HOL/Import/HOL/HOL4Real.thy	Fri May 21 21:42:05 2004 +0200
1.3 @@ -272,10 +272,6 @@
1.4  lemma REAL_LE_NEGTOTAL: "ALL x::real. (0::real) <= x | (0::real) <= - x"
1.5    by (import real REAL_LE_NEGTOTAL)
1.6
1.7 -lemma REAL_LE_MUL: "ALL (x::real) y::real.
1.8 -   (0::real) <= x & (0::real) <= y --> (0::real) <= x * y"
1.9 -  by (import real REAL_LE_MUL)
1.10 -
1.11  lemma REAL_LT_ADDNEG: "ALL (x::real) (y::real) z::real. (y < x + - z) = (y + z < x)"
1.13
1.14 @@ -285,8 +281,11 @@
1.15  lemma REAL_LT_ADD1: "ALL (x::real) y::real. x <= y --> x < y + (1::real)"
1.17
1.18 -lemma REAL_LE_DOUBLE: "ALL x::real. ((0::real) <= x + x) = ((0::real) <= x)"
1.19 -  by (import real REAL_LE_DOUBLE)
1.20 +lemma REAL_SUB_ADD2: "ALL (x::real) y::real. y + (x - y) = x"
1.21 +  by (import real REAL_SUB_ADD2)
1.22 +
1.23 +lemma REAL_ADD_SUB: "ALL (x::real) y::real. x + y - x = y"
1.24 +  by (import real REAL_ADD_SUB)
1.25
1.26  lemma REAL_NEG_EQ: "ALL (x::real) y::real. (- x = y) = (x = - y)"
1.27    by (import real REAL_NEG_EQ)
1.28 @@ -691,9 +690,6 @@
1.29  lemma SUM_CANCEL: "ALL f n d. real.sum (n, d) (%n. f (Suc n) - f n) = f (n + d) - f n"
1.30    by (import real SUM_CANCEL)
1.31
1.32 -lemma REAL_LE_RNEG: "ALL (x::real) y::real. (x <= - y) = (x + y <= (0::real))"
1.33 -  by (import real REAL_LE_RNEG)
1.34 -
1.35  lemma REAL_EQ_RDIV_EQ: "ALL (x::real) (xa::real) xb::real.
1.36     (0::real) < xb --> (x = xa / xb) = (x * xb = xa)"
1.37    by (import real REAL_EQ_RDIV_EQ)
```
```     2.1 --- a/src/HOL/Import/HOL/arithmetic.imp	Fri May 21 21:28:58 2004 +0200
2.2 +++ b/src/HOL/Import/HOL/arithmetic.imp	Fri May 21 21:42:05 2004 +0200
2.3 @@ -166,8 +166,8 @@
2.4    "LESS_MONO_REV" > "Nat.Suc_less_SucD"
2.5    "LESS_MONO_MULT" > "Nat.mult_le_mono1"
2.6    "LESS_MONO_EQ" > "Nat.Suc_less_eq"
2.12    "LESS_MOD" > "Divides.mod_less"
2.13    "LESS_LESS_SUC" > "HOL4Base.arithmetic.LESS_LESS_SUC"
2.14 @@ -180,7 +180,7 @@
2.15    "LESS_EQ_SUC_REFL" > "HOL4Base.arithmetic.LESS_EQ_SUC_REFL"
2.16    "LESS_EQ_SUB_LESS" > "HOL4Base.arithmetic.LESS_EQ_SUB_LESS"
2.17    "LESS_EQ_REFL" > "Nat.le_refl"
2.20    "LESS_EQ_MONO" > "Nat.Suc_le_mono"
2.21    "LESS_EQ_LESS_TRANS" > "Nat.le_less_trans"
```
```     3.1 --- a/src/HOL/Import/HOL/real.imp	Fri May 21 21:28:58 2004 +0200
3.2 +++ b/src/HOL/Import/HOL/real.imp	Fri May 21 21:42:05 2004 +0200
3.3 @@ -25,7 +25,7 @@
3.4    "sumc" > "HOL4Real.real.sumc"
3.5    "sum_def" > "HOL4Real.real.sum_def"
3.6    "sum" > "HOL4Real.real.sum"
3.7 -  "real_sub" > "Ring_and_Field.compare_rls_1"
3.8 +  "real_sub" > "OrderedGroup.compare_rls_1"
3.9    "real_of_num" > "HOL4Compat.real_of_num"
3.10    "real_lte" > "HOL4Compat.real_lte"
3.11    "real_lt" > "HOL.linorder_not_le"
3.12 @@ -74,21 +74,21 @@
3.13    "REAL_SUB_TRIANGLE" > "HOL4Real.real.REAL_SUB_TRIANGLE"
3.14    "REAL_SUB_SUB2" > "HOL4Real.real.REAL_SUB_SUB2"
3.15    "REAL_SUB_SUB" > "HOL4Real.real.REAL_SUB_SUB"
3.16 -  "REAL_SUB_RZERO" > "Ring_and_Field.diff_0_right"
3.18 -  "REAL_SUB_REFL" > "Ring_and_Field.diff_self"
3.19 +  "REAL_SUB_RZERO" > "OrderedGroup.diff_0_right"
3.21 +  "REAL_SUB_REFL" > "OrderedGroup.diff_self"
3.22    "REAL_SUB_RDISTRIB" > "Ring_and_Field.ring_eq_simps_6"
3.23    "REAL_SUB_NEG2" > "HOL4Real.real.REAL_SUB_NEG2"
3.24 -  "REAL_SUB_LZERO" > "Ring_and_Field.diff_0"
3.25 +  "REAL_SUB_LZERO" > "OrderedGroup.diff_0"
3.26    "REAL_SUB_LT" > "RealDef.real_0_less_diff_iff"
3.27    "REAL_SUB_LNEG" > "HOL4Real.real.REAL_SUB_LNEG"
3.28    "REAL_SUB_LE" > "RealDef.real_0_le_diff_iff"
3.29    "REAL_SUB_LDISTRIB" > "Ring_and_Field.ring_eq_simps_7"
3.30    "REAL_SUB_INV2" > "HOL4Real.real.REAL_SUB_INV2"
3.35    "REAL_SUB_ABS" > "HOL4Real.real.REAL_SUB_ABS"
3.36 -  "REAL_SUB_0" > "Ring_and_Field.eq_iff_diff_eq_0"
3.37 +  "REAL_SUB_0" > "OrderedGroup.eq_iff_diff_eq_0"
3.39    "REAL_RINV_UNIQ" > "RealDef.real_inverse_unique"
3.40    "REAL_RDISTRIB" > "Ring_and_Field.ring_eq_simps_4"
3.41 @@ -113,31 +113,31 @@
3.42    "REAL_NZ_IMP_LT" > "HOL4Real.real.REAL_NZ_IMP_LT"
3.43    "REAL_NOT_LT" > "HOL4Compat.real_lte"
3.44    "REAL_NOT_LE" > "HOL.linorder_not_le"
3.45 -  "REAL_NEG_SUB" > "Ring_and_Field.minus_diff_eq"
3.46 +  "REAL_NEG_SUB" > "OrderedGroup.minus_diff_eq"
3.47    "REAL_NEG_RMUL" > "Ring_and_Field.minus_mult_right"
3.48 -  "REAL_NEG_NEG" > "Ring_and_Field.minus_minus"
3.49 +  "REAL_NEG_NEG" > "OrderedGroup.minus_minus"
3.50    "REAL_NEG_MUL2" > "Ring_and_Field.minus_mult_minus"
3.51    "REAL_NEG_MINUS1" > "HOL4Real.real.REAL_NEG_MINUS1"
3.52 -  "REAL_NEG_LT0" > "Ring_and_Field.neg_less_0_iff_less"
3.53 +  "REAL_NEG_LT0" > "OrderedGroup.neg_less_0_iff_less"
3.54    "REAL_NEG_LMUL" > "Ring_and_Field.minus_mult_left"
3.55 -  "REAL_NEG_LE0" > "Ring_and_Field.neg_le_0_iff_le"
3.56 +  "REAL_NEG_LE0" > "OrderedGroup.neg_le_0_iff_le"
3.57    "REAL_NEG_INV" > "Ring_and_Field.nonzero_inverse_minus_eq"
3.58 -  "REAL_NEG_GT0" > "Ring_and_Field.neg_0_less_iff_less"
3.59 -  "REAL_NEG_GE0" > "Ring_and_Field.neg_0_le_iff_le"
3.60 -  "REAL_NEG_EQ0" > "Ring_and_Field.neg_equal_0_iff_equal"
3.61 +  "REAL_NEG_GT0" > "OrderedGroup.neg_0_less_iff_less"
3.62 +  "REAL_NEG_GE0" > "OrderedGroup.neg_0_le_iff_le"
3.63 +  "REAL_NEG_EQ0" > "OrderedGroup.neg_equal_0_iff_equal"
3.64    "REAL_NEG_EQ" > "HOL4Real.real.REAL_NEG_EQ"
3.66 -  "REAL_NEG_0" > "Ring_and_Field.minus_zero"
3.67 -  "REAL_NEGNEG" > "Ring_and_Field.minus_minus"
3.69 +  "REAL_NEG_0" > "OrderedGroup.minus_zero"
3.70 +  "REAL_NEGNEG" > "OrderedGroup.minus_minus"
3.71    "REAL_MUL_SYM" > "Ring_and_Field.ring_eq_simps_2"
3.72    "REAL_MUL_RZERO" > "Ring_and_Field.mult_zero_right"
3.73    "REAL_MUL_RNEG" > "Ring_and_Field.minus_mult_right"
3.74    "REAL_MUL_RINV" > "Ring_and_Field.right_inverse"
3.75 -  "REAL_MUL_RID" > "Ring_and_Field.mult_1_right"
3.76 +  "REAL_MUL_RID" > "OrderedGroup.monoid_mult.mult_1_right"
3.77    "REAL_MUL_LZERO" > "Ring_and_Field.mult_zero_left"
3.78    "REAL_MUL_LNEG" > "Ring_and_Field.minus_mult_left"
3.79    "REAL_MUL_LINV" > "HOL4Compat.REAL_MUL_LINV"
3.80 -  "REAL_MUL_LID" > "Ring_and_Field.almost_semiring.mult_1"
3.81 +  "REAL_MUL_LID" > "OrderedGroup.comm_monoid_mult.mult_1"
3.82    "REAL_MUL_ASSOC" > "HOL4Compat.REAL_MUL_ASSOC"
3.83    "REAL_MUL" > "RealDef.real_of_nat_mult"
3.84    "REAL_MIDDLE2" > "HOL4Real.real.REAL_MIDDLE2"
3.85 @@ -145,33 +145,33 @@
3.86    "REAL_MEAN" > "Ring_and_Field.dense"
3.87    "REAL_LT_TRANS" > "Set.basic_trans_rules_21"
3.88    "REAL_LT_TOTAL" > "HOL4Compat.REAL_LT_TOTAL"
3.91 -  "REAL_LT_RMUL_IMP" > "Ring_and_Field.mult_strict_right_mono"
3.94 +  "REAL_LT_RMUL_IMP" > "Ring_and_Field.ordered_semiring_strict.mult_strict_right_mono"
3.95    "REAL_LT_RMUL_0" > "HOL4Real.real.REAL_LT_RMUL_0"
3.96    "REAL_LT_RMUL" > "RealDef.real_mult_less_iff1"
3.97    "REAL_LT_REFL" > "HOL.order_less_irrefl"
3.98    "REAL_LT_RDIV_EQ" > "Ring_and_Field.pos_less_divide_eq"
3.99    "REAL_LT_RDIV_0" > "HOL4Real.real.REAL_LT_RDIV_0"
3.100    "REAL_LT_RDIV" > "HOL4Real.real.REAL_LT_RDIV"
3.103    "REAL_LT_NZ" > "HOL4Real.real.REAL_LT_NZ"
3.104    "REAL_LT_NEGTOTAL" > "HOL4Real.real.REAL_LT_NEGTOTAL"
3.105 -  "REAL_LT_NEG" > "Ring_and_Field.neg_less_iff_less"
3.106 +  "REAL_LT_NEG" > "OrderedGroup.neg_less_iff_less"
3.107    "REAL_LT_MULTIPLE" > "HOL4Real.real.REAL_LT_MULTIPLE"
3.108    "REAL_LT_MUL2" > "Ring_and_Field.mult_strict_mono'"
3.109    "REAL_LT_MUL" > "Ring_and_Field.mult_pos"
3.110 -  "REAL_LT_LMUL_IMP" > "Ring_and_Field.almost_ordered_semiring.mult_strict_left_mono"
3.111 +  "REAL_LT_LMUL_IMP" > "Ring_and_Field.ordered_comm_semiring_strict.mult_strict_mono"
3.112    "REAL_LT_LMUL_0" > "HOL4Real.real.REAL_LT_LMUL_0"
3.113    "REAL_LT_LMUL" > "HOL4Real.real.REAL_LT_LMUL"
3.114    "REAL_LT_LE" > "HOL.order.order_less_le"
3.115    "REAL_LT_LDIV_EQ" > "Ring_and_Field.pos_divide_less_eq"
3.118    "REAL_LT_INV_EQ" > "Ring_and_Field.inverse_positive_iff_positive"
3.119    "REAL_LT_INV" > "Ring_and_Field.less_imp_inverse_less"
3.120    "REAL_LT_IMP_NE" > "HOL.less_imp_neq"
3.121    "REAL_LT_IMP_LE" > "HOL.order_less_imp_le"
3.124    "REAL_LT_HALF2" > "HOL4Real.real.REAL_LT_HALF2"
3.125    "REAL_LT_HALF1" > "NatSimprocs.half_gt_zero_iff"
3.126    "REAL_LT_GT" > "HOL.order_less_not_sym"
3.127 @@ -179,20 +179,20 @@
3.128    "REAL_LT_FRACTION" > "HOL4Real.real.REAL_LT_FRACTION"
3.129    "REAL_LT_DIV" > "HOL4Real.real.REAL_LT_DIV"
3.130    "REAL_LT_ANTISYM" > "HOL4Real.real.REAL_LT_ANTISYM"
3.141    "REAL_LT_1" > "HOL4Real.real.REAL_LT_1"
3.142 -  "REAL_LT_01" > "Ring_and_Field.ordered_semiring.zero_less_one"
3.143 +  "REAL_LT_01" > "Ring_and_Field.ordered_semidom.zero_less_one"
3.144    "REAL_LTE_TRANS" > "Set.basic_trans_rules_24"
3.145    "REAL_LTE_TOTAL" > "HOL4Real.real.REAL_LTE_TOTAL"
3.146    "REAL_LTE_ANTSYM" > "HOL4Real.real.REAL_LTE_ANTSYM"
3.150    "REAL_LT1_POW2" > "HOL4Real.real.REAL_LT1_POW2"
3.151    "REAL_LT" > "RealDef.real_of_nat_less_iff"
3.152 @@ -200,46 +200,46 @@
3.153    "REAL_LINV_UNIQ" > "HOL4Real.real.REAL_LINV_UNIQ"
3.154    "REAL_LE_TRANS" > "Set.basic_trans_rules_25"
3.155    "REAL_LE_TOTAL" > "HOL.linorder.linorder_linear"
3.160    "REAL_LE_SQUARE" > "Ring_and_Field.zero_le_square"
3.161 -  "REAL_LE_RNEG" > "HOL4Real.real.REAL_LE_RNEG"
3.162 -  "REAL_LE_RMUL_IMP" > "Ring_and_Field.mult_right_mono"
3.163 +  "REAL_LE_RNEG" > "OrderedGroup.le_eq_neg"
3.164 +  "REAL_LE_RMUL_IMP" > "Ring_and_Field.pordered_semiring.mult_right_mono"
3.165    "REAL_LE_RMUL" > "RealDef.real_mult_le_cancel_iff1"
3.166    "REAL_LE_REFL" > "HOL.order.order_refl"
3.167    "REAL_LE_RDIV_EQ" > "Ring_and_Field.pos_le_divide_eq"
3.168    "REAL_LE_RDIV" > "HOL4Real.real.REAL_LE_RDIV"
3.171    "REAL_LE_POW2" > "NatBin.zero_le_power2"
3.172    "REAL_LE_NEGTOTAL" > "HOL4Real.real.REAL_LE_NEGTOTAL"
3.173 -  "REAL_LE_NEGR" > "Ring_and_Field.le_minus_self_iff"
3.174 -  "REAL_LE_NEGL" > "Ring_and_Field.minus_le_self_iff"
3.175 -  "REAL_LE_NEG2" > "Ring_and_Field.neg_le_iff_le"
3.176 -  "REAL_LE_NEG" > "Ring_and_Field.neg_le_iff_le"
3.177 +  "REAL_LE_NEGR" > "OrderedGroup.le_minus_self_iff"
3.178 +  "REAL_LE_NEGL" > "OrderedGroup.minus_le_self_iff"
3.179 +  "REAL_LE_NEG2" > "OrderedGroup.neg_le_iff_le"
3.180 +  "REAL_LE_NEG" > "OrderedGroup.neg_le_iff_le"
3.181    "REAL_LE_MUL2" > "HOL4Real.real.REAL_LE_MUL2"
3.182 -  "REAL_LE_MUL" > "HOL4Real.real.REAL_LE_MUL"
3.183 +  "REAL_LE_MUL" > "Ring_and_Field.mult_pos_le"
3.184    "REAL_LE_LT" > "HOL.order_le_less"
3.186 -  "REAL_LE_LMUL_IMP" > "Ring_and_Field.mult_left_mono"
3.187 +  "REAL_LE_LMUL_IMP" > "Ring_and_Field.pordered_comm_semiring.mult_mono"
3.188    "REAL_LE_LMUL" > "RealDef.real_mult_le_cancel_iff2"
3.189    "REAL_LE_LDIV_EQ" > "Ring_and_Field.pos_divide_le_eq"
3.190    "REAL_LE_LDIV" > "HOL4Real.real.REAL_LE_LDIV"
3.195    "REAL_LE_INV_EQ" > "Ring_and_Field.inverse_nonnegative_iff_nonnegative"
3.196    "REAL_LE_INV" > "HOL4Real.real.REAL_LE_INV"
3.197 -  "REAL_LE_DOUBLE" > "HOL4Real.real.REAL_LE_DOUBLE"
3.199    "REAL_LE_DIV" > "HOL4Real.real.REAL_LE_DIV"
3.200    "REAL_LE_ANTISYM" > "HOL.order_eq_iff"
3.206    "REAL_LE_01" > "Ring_and_Field.zero_le_one"
3.207    "REAL_LET_TRANS" > "Set.basic_trans_rules_23"
3.208    "REAL_LET_TOTAL" > "HOL4Real.real.REAL_LET_TOTAL"
3.209    "REAL_LET_ANTISYM" > "HOL4Real.real.REAL_LET_ANTISYM"
3.213    "REAL_LE1_POW2" > "HOL4Real.real.REAL_LE1_POW2"
3.214    "REAL_LE" > "RealDef.real_of_nat_le_iff"
3.215 @@ -262,14 +262,14 @@
3.216    "REAL_EQ_RMUL_IMP" > "Ring_and_Field.field_mult_cancel_right_lemma"
3.217    "REAL_EQ_RMUL" > "Ring_and_Field.field_mult_cancel_right"
3.218    "REAL_EQ_RDIV_EQ" > "HOL4Real.real.REAL_EQ_RDIV_EQ"
3.220 -  "REAL_EQ_NEG" > "Ring_and_Field.neg_equal_iff_equal"
3.222 +  "REAL_EQ_NEG" > "OrderedGroup.neg_equal_iff_equal"
3.223    "REAL_EQ_MUL_LCANCEL" > "Ring_and_Field.field_mult_cancel_left"
3.224    "REAL_EQ_LMUL_IMP" > "HOL4Real.real.REAL_EQ_LMUL_IMP"
3.225    "REAL_EQ_LMUL2" > "RealDef.real_mult_left_cancel"
3.226    "REAL_EQ_LMUL" > "Ring_and_Field.field_mult_cancel_left"
3.227    "REAL_EQ_LDIV_EQ" > "HOL4Real.real.REAL_EQ_LDIV_EQ"
3.230    "REAL_EQ_IMP_LE" > "HOL.order_eq_refl"
3.231    "REAL_ENTIRE" > "Ring_and_Field.field_mult_eq_0_iff"
3.232    "REAL_DOWN2" > "RealDef.real_lbound_gt_zero"
3.233 @@ -285,22 +285,22 @@
3.234    "REAL_ARCH" > "RComplete.reals_Archimedean3"
3.253 -  "REAL_ABS_TRIANGLE" > "Ring_and_Field.abs_triangle_ineq"
3.254 -  "REAL_ABS_POS" > "Ring_and_Field.abs_ge_zero"
3.255 +  "REAL_ABS_TRIANGLE" > "OrderedGroup.abs_triangle_ineq"
3.256 +  "REAL_ABS_POS" > "OrderedGroup.abs_ge_zero"
3.257    "REAL_ABS_MUL" > "Ring_and_Field.abs_mult"
3.258 -  "REAL_ABS_0" > "Ring_and_Field.abs_zero"
3.259 +  "REAL_ABS_0" > "OrderedGroup.abs_zero"
3.260    "REAL_10" > "HOL4Compat.REAL_10"
3.261    "REAL_1" > "HOL4Real.real.REAL_1"
3.262    "REAL_0" > "HOL4Real.real.REAL_0"
3.263 @@ -326,8 +326,8 @@
3.264    "POW_2" > "NatBin.power2_eq_square"
3.265    "POW_1" > "Power.power_one_right"
3.266    "POW_0" > "Power.power_0_Suc"
3.267 -  "ABS_ZERO" > "Ring_and_Field.abs_zero_iff"
3.268 -  "ABS_TRIANGLE" > "Ring_and_Field.abs_triangle_ineq"
3.269 +  "ABS_ZERO" > "OrderedGroup.abs_eq_0"
3.270 +  "ABS_TRIANGLE" > "OrderedGroup.abs_triangle_ineq"
3.271    "ABS_SUM" > "HOL4Real.real.ABS_SUM"
3.272    "ABS_SUB_ABS" > "HOL4Real.real.ABS_SUB_ABS"
3.273    "ABS_SUB" > "HOL4Real.real.ABS_SUB"
3.274 @@ -336,13 +336,13 @@
3.275    "ABS_SIGN" > "HOL4Real.real.ABS_SIGN"
3.276    "ABS_REFL" > "HOL4Real.real.ABS_REFL"
3.277    "ABS_POW2" > "NatBin.abs_power2"
3.278 -  "ABS_POS" > "Ring_and_Field.abs_ge_zero"
3.279 -  "ABS_NZ" > "Ring_and_Field.zero_less_abs_iff"
3.280 -  "ABS_NEG" > "Ring_and_Field.abs_minus_cancel"
3.281 +  "ABS_POS" > "OrderedGroup.abs_ge_zero"
3.282 +  "ABS_NZ" > "OrderedGroup.zero_less_abs_iff"
3.283 +  "ABS_NEG" > "OrderedGroup.abs_minus_cancel"
3.284    "ABS_N" > "RealDef.abs_real_of_nat_cancel"
3.285    "ABS_MUL" > "Ring_and_Field.abs_mult"
3.286    "ABS_LT_MUL2" > "HOL4Real.real.ABS_LT_MUL2"
3.287 -  "ABS_LE" > "Ring_and_Field.abs_ge_self"
3.288 +  "ABS_LE" > "OrderedGroup.abs_ge_self"
3.289    "ABS_INV" > "Ring_and_Field.nonzero_abs_inverse"
3.290    "ABS_DIV" > "Ring_and_Field.nonzero_abs_divide"
3.291    "ABS_CIRCLE" > "HOL4Real.real.ABS_CIRCLE"
3.292 @@ -352,8 +352,8 @@
3.293    "ABS_BETWEEN2" > "HOL4Real.real.ABS_BETWEEN2"
3.294    "ABS_BETWEEN1" > "HOL4Real.real.ABS_BETWEEN1"
3.295    "ABS_BETWEEN" > "HOL4Real.real.ABS_BETWEEN"
3.296 -  "ABS_ABS" > "Ring_and_Field.abs_idempotent"
3.297 +  "ABS_ABS" > "OrderedGroup.abs_idempotent"
3.298    "ABS_1" > "Ring_and_Field.abs_one"
3.299 -  "ABS_0" > "Ring_and_Field.abs_zero"
3.300 +  "ABS_0" > "OrderedGroup.abs_zero"
3.301
3.302  end
```
```     4.1 --- a/src/HOL/Import/HOL/realax.imp	Fri May 21 21:28:58 2004 +0200
4.2 +++ b/src/HOL/Import/HOL/realax.imp	Fri May 21 21:42:05 2004 +0200
4.3 @@ -93,18 +93,18 @@
4.4    "REAL_SUP_ALLPOS" > "HOL4Compat.REAL_SUP_ALLPOS"
4.5    "REAL_MUL_SYM" > "Ring_and_Field.ring_eq_simps_2"
4.6    "REAL_MUL_LINV" > "HOL4Compat.REAL_MUL_LINV"
4.7 -  "REAL_MUL_LID" > "Ring_and_Field.almost_semiring.mult_1"
4.8 +  "REAL_MUL_LID" > "OrderedGroup.comm_monoid_mult.mult_1"
4.9    "REAL_MUL_ASSOC" > "HOL4Compat.REAL_MUL_ASSOC"
4.10    "REAL_LT_TRANS" > "Set.basic_trans_rules_21"
4.11    "REAL_LT_TOTAL" > "HOL4Compat.REAL_LT_TOTAL"
4.12    "REAL_LT_REFL" > "HOL.order_less_irrefl"
4.13    "REAL_LT_MUL" > "Ring_and_Field.mult_pos"