updated;
authorwenzelm
Fri May 21 21:42:05 2004 +0200 (2004-05-21)
changeset 147961e83aa391ade
parent 14795 b702848de41f
child 14797 546365fe8349
updated;
src/HOL/Import/HOL/HOL4Real.thy
src/HOL/Import/HOL/arithmetic.imp
src/HOL/Import/HOL/real.imp
src/HOL/Import/HOL/realax.imp
     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.12    by (import real REAL_LT_ADDNEG)
    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.16    by (import real REAL_LT_ADD1)
    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.7 -  "LESS_MONO_ADD_INV" > "Ring_and_Field.add_less_imp_less_right"
     2.8 -  "LESS_MONO_ADD_EQ" > "Ring_and_Field.add_less_cancel_right"
     2.9 +  "LESS_MONO_ADD_INV" > "OrderedGroup.add_less_imp_less_right"
    2.10 +  "LESS_MONO_ADD_EQ" > "OrderedGroup.add_less_cancel_right"
    2.11    "LESS_MONO_ADD" > "Nat.add_less_mono1"
    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.18 -  "LESS_EQ_MONO_ADD_EQ" > "Ring_and_Field.add_le_cancel_right"
    2.19 +  "LESS_EQ_MONO_ADD_EQ" > "OrderedGroup.add_le_cancel_right"
    2.20    "LESS_EQ_MONO" > "Nat.Suc_le_mono"
    2.21    "LESS_EQ_LESS_TRANS" > "Nat.le_less_trans"
    2.22    "LESS_EQ_LESS_EQ_MONO" > "Nat.add_le_mono"
     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.17 -  "REAL_SUB_RNEG" > "Ring_and_Field.diff_minus_eq_add"
    3.18 -  "REAL_SUB_REFL" > "Ring_and_Field.diff_self"
    3.19 +  "REAL_SUB_RZERO" > "OrderedGroup.diff_0_right"
    3.20 +  "REAL_SUB_RNEG" > "OrderedGroup.diff_minus_eq_add"
    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.31 -  "REAL_SUB_ADD2" > "Ring_and_Field.add_minus_self_left"
    3.32 -  "REAL_SUB_ADD" > "Ring_and_Field.minus_add_self"
    3.33 +  "REAL_SUB_ADD2" > "HOL4Real.real.REAL_SUB_ADD2"
    3.34 +  "REAL_SUB_ADD" > "OrderedGroup.diff_add_cancel"
    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.38    "REAL_RNEG_UNIQ" > "RealDef.real_add_eq_0_iff"
    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.65 -  "REAL_NEG_ADD" > "Ring_and_Field.minus_add_distrib"
    3.66 -  "REAL_NEG_0" > "Ring_and_Field.minus_zero"
    3.67 -  "REAL_NEGNEG" > "Ring_and_Field.minus_minus"
    3.68 +  "REAL_NEG_ADD" > "OrderedGroup.minus_add_distrib"
    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.89 -  "REAL_LT_SUB_RADD" > "Ring_and_Field.compare_rls_6"
    3.90 -  "REAL_LT_SUB_LADD" > "Ring_and_Field.compare_rls_7"
    3.91 -  "REAL_LT_RMUL_IMP" > "Ring_and_Field.mult_strict_right_mono"
    3.92 +  "REAL_LT_SUB_RADD" > "OrderedGroup.compare_rls_6"
    3.93 +  "REAL_LT_SUB_LADD" > "OrderedGroup.compare_rls_7"
    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.101 -  "REAL_LT_RADD" > "Ring_and_Field.add_less_cancel_right"
   3.102 +  "REAL_LT_RADD" > "OrderedGroup.add_less_cancel_right"
   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.116 -  "REAL_LT_LADD" > "Ring_and_Field.add_less_cancel_left"
   3.117 +  "REAL_LT_LADD" > "OrderedGroup.add_less_cancel_left"
   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.122 -  "REAL_LT_IADD" > "Ring_and_Field.add_strict_left_mono"
   3.123 +  "REAL_LT_IADD" > "OrderedGroup.add_strict_left_mono"
   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.131 -  "REAL_LT_ADD_SUB" > "Ring_and_Field.compare_rls_7"
   3.132 +  "REAL_LT_ADD_SUB" > "OrderedGroup.compare_rls_7"
   3.133    "REAL_LT_ADDR" > "HOL4Real.real.REAL_LT_ADDR"
   3.134    "REAL_LT_ADDNEG2" > "HOL4Real.real.REAL_LT_ADDNEG2"
   3.135    "REAL_LT_ADDNEG" > "HOL4Real.real.REAL_LT_ADDNEG"
   3.136    "REAL_LT_ADDL" > "HOL4Real.real.REAL_LT_ADDL"
   3.137 -  "REAL_LT_ADD2" > "Ring_and_Field.add_strict_mono"
   3.138 +  "REAL_LT_ADD2" > "OrderedGroup.add_strict_mono"
   3.139    "REAL_LT_ADD1" > "HOL4Real.real.REAL_LT_ADD1"
   3.140    "REAL_LT_ADD" > "RealDef.real_add_order"
   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.147 -  "REAL_LTE_ADD2" > "Ring_and_Field.add_less_le_mono"
   3.148 +  "REAL_LTE_ADD2" > "OrderedGroup.add_less_le_mono"
   3.149    "REAL_LTE_ADD" > "HOL4Real.real.REAL_LTE_ADD"
   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.156 -  "REAL_LE_SUB_RADD" > "Ring_and_Field.compare_rls_8"
   3.157 -  "REAL_LE_SUB_LADD" > "Ring_and_Field.compare_rls_9"
   3.158 +  "REAL_LE_SUB_RADD" > "OrderedGroup.compare_rls_8"
   3.159 +  "REAL_LE_SUB_LADD" > "OrderedGroup.compare_rls_9"
   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.169 -  "REAL_LE_RADD" > "Ring_and_Field.add_le_cancel_right"
   3.170 +  "REAL_LE_RADD" > "OrderedGroup.add_le_cancel_right"
   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.185    "REAL_LE_LNEG" > "RealDef.real_0_le_add_iff"
   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.191 -  "REAL_LE_LADD_IMP" > "Ring_and_Field.almost_ordered_semiring.add_left_mono"
   3.192 -  "REAL_LE_LADD" > "Ring_and_Field.add_le_cancel_left"
   3.193 +  "REAL_LE_LADD_IMP" > "OrderedGroup.pordered_ab_semigroup_add.add_left_mono"
   3.194 +  "REAL_LE_LADD" > "OrderedGroup.add_le_cancel_left"
   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.198 +  "REAL_LE_DOUBLE" > "OrderedGroup.zero_le_double_add_iff_zero_le_single_add"
   3.199    "REAL_LE_DIV" > "HOL4Real.real.REAL_LE_DIV"
   3.200    "REAL_LE_ANTISYM" > "HOL.order_eq_iff"
   3.201    "REAL_LE_ADDR" > "HOL4Real.real.REAL_LE_ADDR"
   3.202    "REAL_LE_ADDL" > "HOL4Real.real.REAL_LE_ADDL"
   3.203 -  "REAL_LE_ADD2" > "Ring_and_Field.add_mono"
   3.204 +  "REAL_LE_ADD2" > "OrderedGroup.add_mono"
   3.205    "REAL_LE_ADD" > "RealDef.real_le_add_order"
   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.210 -  "REAL_LET_ADD2" > "Ring_and_Field.add_le_less_mono"
   3.211 +  "REAL_LET_ADD2" > "OrderedGroup.add_le_less_mono"
   3.212    "REAL_LET_ADD" > "HOL4Real.real.REAL_LET_ADD"
   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.219 -  "REAL_EQ_RADD" > "Ring_and_Field.add_right_cancel"
   3.220 -  "REAL_EQ_NEG" > "Ring_and_Field.neg_equal_iff_equal"
   3.221 +  "REAL_EQ_RADD" > "OrderedGroup.add_right_cancel"
   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.228 -  "REAL_EQ_LADD" > "Ring_and_Field.add_left_cancel"
   3.229 +  "REAL_EQ_LADD" > "OrderedGroup.add_left_cancel"
   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.235    "REAL_ADD_SYM" > "Ring_and_Field.ring_eq_simps_9"
   3.236    "REAL_ADD_SUB2" > "HOL4Real.real.REAL_ADD_SUB2"
   3.237 -  "REAL_ADD_SUB" > "Ring_and_Field.add_minus_self_right"
   3.238 -  "REAL_ADD_RINV" > "Ring_and_Field.right_minus"
   3.239 +  "REAL_ADD_SUB" > "HOL4Real.real.REAL_ADD_SUB"
   3.240 +  "REAL_ADD_RINV" > "OrderedGroup.right_minus"
   3.241    "REAL_ADD_RID_UNIQ" > "HOL4Real.real.REAL_ADD_RID_UNIQ"
   3.242 -  "REAL_ADD_RID" > "Ring_and_Field.add_0_right"
   3.243 +  "REAL_ADD_RID" > "OrderedGroup.add_0_right"
   3.244    "REAL_ADD_RDISTRIB" > "Ring_and_Field.ring_eq_simps_4"
   3.245    "REAL_ADD_LINV" > "HOL4Compat.REAL_ADD_LINV"
   3.246    "REAL_ADD_LID_UNIQ" > "HOL4Real.real.REAL_ADD_LID_UNIQ"
   3.247 -  "REAL_ADD_LID" > "Ring_and_Field.abelian_semigroup.add_0"
   3.248 +  "REAL_ADD_LID" > "OrderedGroup.comm_monoid_add.add_0"
   3.249    "REAL_ADD_LDISTRIB" > "Ring_and_Field.ring_eq_simps_5"
   3.250    "REAL_ADD_ASSOC" > "HOL4Compat.REAL_ADD_ASSOC"
   3.251    "REAL_ADD2_SUB2" > "HOL4Real.real.REAL_ADD2_SUB2"
   3.252    "REAL_ADD" > "RealDef.real_of_nat_add"
   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"
    4.14 -  "REAL_LT_IADD" > "Ring_and_Field.add_strict_left_mono"
    4.15 +  "REAL_LT_IADD" > "OrderedGroup.add_strict_left_mono"
    4.16    "REAL_LDISTRIB" > "Ring_and_Field.ring_eq_simps_5"
    4.17    "REAL_INV_0" > "Ring_and_Field.division_by_zero.inverse_zero"
    4.18    "REAL_ADD_SYM" > "Ring_and_Field.ring_eq_simps_9"
    4.19    "REAL_ADD_LINV" > "HOL4Compat.REAL_ADD_LINV"
    4.20 -  "REAL_ADD_LID" > "Ring_and_Field.abelian_semigroup.add_0"
    4.21 +  "REAL_ADD_LID" > "OrderedGroup.comm_monoid_add.add_0"
    4.22    "REAL_ADD_ASSOC" > "HOL4Compat.REAL_ADD_ASSOC"
    4.23    "REAL_10" > "HOL4Compat.REAL_10"
    4.24    "HREAL_RDISTRIB" > "HOL4Real.realax.HREAL_RDISTRIB"