# HG changeset patch # User wenzelm # Date 1085168525 -7200 # Node ID 1e83aa391ade47e30947a65fdc1d15709ec17fd4 # Parent b702848de41fbc6d22bd3366120c44e79ce10185 updated; diff -r b702848de41f -r 1e83aa391ade src/HOL/Import/HOL/HOL4Real.thy --- a/src/HOL/Import/HOL/HOL4Real.thy Fri May 21 21:28:58 2004 +0200 +++ b/src/HOL/Import/HOL/HOL4Real.thy Fri May 21 21:42:05 2004 +0200 @@ -272,10 +272,6 @@ lemma REAL_LE_NEGTOTAL: "ALL x::real. (0::real) <= x | (0::real) <= - x" by (import real REAL_LE_NEGTOTAL) -lemma REAL_LE_MUL: "ALL (x::real) y::real. - (0::real) <= x & (0::real) <= y --> (0::real) <= x * y" - by (import real REAL_LE_MUL) - lemma REAL_LT_ADDNEG: "ALL (x::real) (y::real) z::real. (y < x + - z) = (y + z < x)" by (import real REAL_LT_ADDNEG) @@ -285,8 +281,11 @@ lemma REAL_LT_ADD1: "ALL (x::real) y::real. x <= y --> x < y + (1::real)" by (import real REAL_LT_ADD1) -lemma REAL_LE_DOUBLE: "ALL x::real. ((0::real) <= x + x) = ((0::real) <= x)" - by (import real REAL_LE_DOUBLE) +lemma REAL_SUB_ADD2: "ALL (x::real) y::real. y + (x - y) = x" + by (import real REAL_SUB_ADD2) + +lemma REAL_ADD_SUB: "ALL (x::real) y::real. x + y - x = y" + by (import real REAL_ADD_SUB) lemma REAL_NEG_EQ: "ALL (x::real) y::real. (- x = y) = (x = - y)" by (import real REAL_NEG_EQ) @@ -691,9 +690,6 @@ lemma SUM_CANCEL: "ALL f n d. real.sum (n, d) (%n. f (Suc n) - f n) = f (n + d) - f n" by (import real SUM_CANCEL) -lemma REAL_LE_RNEG: "ALL (x::real) y::real. (x <= - y) = (x + y <= (0::real))" - by (import real REAL_LE_RNEG) - lemma REAL_EQ_RDIV_EQ: "ALL (x::real) (xa::real) xb::real. (0::real) < xb --> (x = xa / xb) = (x * xb = xa)" by (import real REAL_EQ_RDIV_EQ) diff -r b702848de41f -r 1e83aa391ade src/HOL/Import/HOL/arithmetic.imp --- a/src/HOL/Import/HOL/arithmetic.imp Fri May 21 21:28:58 2004 +0200 +++ b/src/HOL/Import/HOL/arithmetic.imp Fri May 21 21:42:05 2004 +0200 @@ -166,8 +166,8 @@ "LESS_MONO_REV" > "Nat.Suc_less_SucD" "LESS_MONO_MULT" > "Nat.mult_le_mono1" "LESS_MONO_EQ" > "Nat.Suc_less_eq" - "LESS_MONO_ADD_INV" > "Ring_and_Field.add_less_imp_less_right" - "LESS_MONO_ADD_EQ" > "Ring_and_Field.add_less_cancel_right" + "LESS_MONO_ADD_INV" > "OrderedGroup.add_less_imp_less_right" + "LESS_MONO_ADD_EQ" > "OrderedGroup.add_less_cancel_right" "LESS_MONO_ADD" > "Nat.add_less_mono1" "LESS_MOD" > "Divides.mod_less" "LESS_LESS_SUC" > "HOL4Base.arithmetic.LESS_LESS_SUC" @@ -180,7 +180,7 @@ "LESS_EQ_SUC_REFL" > "HOL4Base.arithmetic.LESS_EQ_SUC_REFL" "LESS_EQ_SUB_LESS" > "HOL4Base.arithmetic.LESS_EQ_SUB_LESS" "LESS_EQ_REFL" > "Nat.le_refl" - "LESS_EQ_MONO_ADD_EQ" > "Ring_and_Field.add_le_cancel_right" + "LESS_EQ_MONO_ADD_EQ" > "OrderedGroup.add_le_cancel_right" "LESS_EQ_MONO" > "Nat.Suc_le_mono" "LESS_EQ_LESS_TRANS" > "Nat.le_less_trans" "LESS_EQ_LESS_EQ_MONO" > "Nat.add_le_mono" diff -r b702848de41f -r 1e83aa391ade src/HOL/Import/HOL/real.imp --- a/src/HOL/Import/HOL/real.imp Fri May 21 21:28:58 2004 +0200 +++ b/src/HOL/Import/HOL/real.imp Fri May 21 21:42:05 2004 +0200 @@ -25,7 +25,7 @@ "sumc" > "HOL4Real.real.sumc" "sum_def" > "HOL4Real.real.sum_def" "sum" > "HOL4Real.real.sum" - "real_sub" > "Ring_and_Field.compare_rls_1" + "real_sub" > "OrderedGroup.compare_rls_1" "real_of_num" > "HOL4Compat.real_of_num" "real_lte" > "HOL4Compat.real_lte" "real_lt" > "HOL.linorder_not_le" @@ -74,21 +74,21 @@ "REAL_SUB_TRIANGLE" > "HOL4Real.real.REAL_SUB_TRIANGLE" "REAL_SUB_SUB2" > "HOL4Real.real.REAL_SUB_SUB2" "REAL_SUB_SUB" > "HOL4Real.real.REAL_SUB_SUB" - "REAL_SUB_RZERO" > "Ring_and_Field.diff_0_right" - "REAL_SUB_RNEG" > "Ring_and_Field.diff_minus_eq_add" - "REAL_SUB_REFL" > "Ring_and_Field.diff_self" + "REAL_SUB_RZERO" > "OrderedGroup.diff_0_right" + "REAL_SUB_RNEG" > "OrderedGroup.diff_minus_eq_add" + "REAL_SUB_REFL" > "OrderedGroup.diff_self" "REAL_SUB_RDISTRIB" > "Ring_and_Field.ring_eq_simps_6" "REAL_SUB_NEG2" > "HOL4Real.real.REAL_SUB_NEG2" - "REAL_SUB_LZERO" > "Ring_and_Field.diff_0" + "REAL_SUB_LZERO" > "OrderedGroup.diff_0" "REAL_SUB_LT" > "RealDef.real_0_less_diff_iff" "REAL_SUB_LNEG" > "HOL4Real.real.REAL_SUB_LNEG" "REAL_SUB_LE" > "RealDef.real_0_le_diff_iff" "REAL_SUB_LDISTRIB" > "Ring_and_Field.ring_eq_simps_7" "REAL_SUB_INV2" > "HOL4Real.real.REAL_SUB_INV2" - "REAL_SUB_ADD2" > "Ring_and_Field.add_minus_self_left" - "REAL_SUB_ADD" > "Ring_and_Field.minus_add_self" + "REAL_SUB_ADD2" > "HOL4Real.real.REAL_SUB_ADD2" + "REAL_SUB_ADD" > "OrderedGroup.diff_add_cancel" "REAL_SUB_ABS" > "HOL4Real.real.REAL_SUB_ABS" - "REAL_SUB_0" > "Ring_and_Field.eq_iff_diff_eq_0" + "REAL_SUB_0" > "OrderedGroup.eq_iff_diff_eq_0" "REAL_RNEG_UNIQ" > "RealDef.real_add_eq_0_iff" "REAL_RINV_UNIQ" > "RealDef.real_inverse_unique" "REAL_RDISTRIB" > "Ring_and_Field.ring_eq_simps_4" @@ -113,31 +113,31 @@ "REAL_NZ_IMP_LT" > "HOL4Real.real.REAL_NZ_IMP_LT" "REAL_NOT_LT" > "HOL4Compat.real_lte" "REAL_NOT_LE" > "HOL.linorder_not_le" - "REAL_NEG_SUB" > "Ring_and_Field.minus_diff_eq" + "REAL_NEG_SUB" > "OrderedGroup.minus_diff_eq" "REAL_NEG_RMUL" > "Ring_and_Field.minus_mult_right" - "REAL_NEG_NEG" > "Ring_and_Field.minus_minus" + "REAL_NEG_NEG" > "OrderedGroup.minus_minus" "REAL_NEG_MUL2" > "Ring_and_Field.minus_mult_minus" "REAL_NEG_MINUS1" > "HOL4Real.real.REAL_NEG_MINUS1" - "REAL_NEG_LT0" > "Ring_and_Field.neg_less_0_iff_less" + "REAL_NEG_LT0" > "OrderedGroup.neg_less_0_iff_less" "REAL_NEG_LMUL" > "Ring_and_Field.minus_mult_left" - "REAL_NEG_LE0" > "Ring_and_Field.neg_le_0_iff_le" + "REAL_NEG_LE0" > "OrderedGroup.neg_le_0_iff_le" "REAL_NEG_INV" > "Ring_and_Field.nonzero_inverse_minus_eq" - "REAL_NEG_GT0" > "Ring_and_Field.neg_0_less_iff_less" - "REAL_NEG_GE0" > "Ring_and_Field.neg_0_le_iff_le" - "REAL_NEG_EQ0" > "Ring_and_Field.neg_equal_0_iff_equal" + "REAL_NEG_GT0" > "OrderedGroup.neg_0_less_iff_less" + "REAL_NEG_GE0" > "OrderedGroup.neg_0_le_iff_le" + "REAL_NEG_EQ0" > "OrderedGroup.neg_equal_0_iff_equal" "REAL_NEG_EQ" > "HOL4Real.real.REAL_NEG_EQ" - "REAL_NEG_ADD" > "Ring_and_Field.minus_add_distrib" - "REAL_NEG_0" > "Ring_and_Field.minus_zero" - "REAL_NEGNEG" > "Ring_and_Field.minus_minus" + "REAL_NEG_ADD" > "OrderedGroup.minus_add_distrib" + "REAL_NEG_0" > "OrderedGroup.minus_zero" + "REAL_NEGNEG" > "OrderedGroup.minus_minus" "REAL_MUL_SYM" > "Ring_and_Field.ring_eq_simps_2" "REAL_MUL_RZERO" > "Ring_and_Field.mult_zero_right" "REAL_MUL_RNEG" > "Ring_and_Field.minus_mult_right" "REAL_MUL_RINV" > "Ring_and_Field.right_inverse" - "REAL_MUL_RID" > "Ring_and_Field.mult_1_right" + "REAL_MUL_RID" > "OrderedGroup.monoid_mult.mult_1_right" "REAL_MUL_LZERO" > "Ring_and_Field.mult_zero_left" "REAL_MUL_LNEG" > "Ring_and_Field.minus_mult_left" "REAL_MUL_LINV" > "HOL4Compat.REAL_MUL_LINV" - "REAL_MUL_LID" > "Ring_and_Field.almost_semiring.mult_1" + "REAL_MUL_LID" > "OrderedGroup.comm_monoid_mult.mult_1" "REAL_MUL_ASSOC" > "HOL4Compat.REAL_MUL_ASSOC" "REAL_MUL" > "RealDef.real_of_nat_mult" "REAL_MIDDLE2" > "HOL4Real.real.REAL_MIDDLE2" @@ -145,33 +145,33 @@ "REAL_MEAN" > "Ring_and_Field.dense" "REAL_LT_TRANS" > "Set.basic_trans_rules_21" "REAL_LT_TOTAL" > "HOL4Compat.REAL_LT_TOTAL" - "REAL_LT_SUB_RADD" > "Ring_and_Field.compare_rls_6" - "REAL_LT_SUB_LADD" > "Ring_and_Field.compare_rls_7" - "REAL_LT_RMUL_IMP" > "Ring_and_Field.mult_strict_right_mono" + "REAL_LT_SUB_RADD" > "OrderedGroup.compare_rls_6" + "REAL_LT_SUB_LADD" > "OrderedGroup.compare_rls_7" + "REAL_LT_RMUL_IMP" > "Ring_and_Field.ordered_semiring_strict.mult_strict_right_mono" "REAL_LT_RMUL_0" > "HOL4Real.real.REAL_LT_RMUL_0" "REAL_LT_RMUL" > "RealDef.real_mult_less_iff1" "REAL_LT_REFL" > "HOL.order_less_irrefl" "REAL_LT_RDIV_EQ" > "Ring_and_Field.pos_less_divide_eq" "REAL_LT_RDIV_0" > "HOL4Real.real.REAL_LT_RDIV_0" "REAL_LT_RDIV" > "HOL4Real.real.REAL_LT_RDIV" - "REAL_LT_RADD" > "Ring_and_Field.add_less_cancel_right" + "REAL_LT_RADD" > "OrderedGroup.add_less_cancel_right" "REAL_LT_NZ" > "HOL4Real.real.REAL_LT_NZ" "REAL_LT_NEGTOTAL" > "HOL4Real.real.REAL_LT_NEGTOTAL" - "REAL_LT_NEG" > "Ring_and_Field.neg_less_iff_less" + "REAL_LT_NEG" > "OrderedGroup.neg_less_iff_less" "REAL_LT_MULTIPLE" > "HOL4Real.real.REAL_LT_MULTIPLE" "REAL_LT_MUL2" > "Ring_and_Field.mult_strict_mono'" "REAL_LT_MUL" > "Ring_and_Field.mult_pos" - "REAL_LT_LMUL_IMP" > "Ring_and_Field.almost_ordered_semiring.mult_strict_left_mono" + "REAL_LT_LMUL_IMP" > "Ring_and_Field.ordered_comm_semiring_strict.mult_strict_mono" "REAL_LT_LMUL_0" > "HOL4Real.real.REAL_LT_LMUL_0" "REAL_LT_LMUL" > "HOL4Real.real.REAL_LT_LMUL" "REAL_LT_LE" > "HOL.order.order_less_le" "REAL_LT_LDIV_EQ" > "Ring_and_Field.pos_divide_less_eq" - "REAL_LT_LADD" > "Ring_and_Field.add_less_cancel_left" + "REAL_LT_LADD" > "OrderedGroup.add_less_cancel_left" "REAL_LT_INV_EQ" > "Ring_and_Field.inverse_positive_iff_positive" "REAL_LT_INV" > "Ring_and_Field.less_imp_inverse_less" "REAL_LT_IMP_NE" > "HOL.less_imp_neq" "REAL_LT_IMP_LE" > "HOL.order_less_imp_le" - "REAL_LT_IADD" > "Ring_and_Field.add_strict_left_mono" + "REAL_LT_IADD" > "OrderedGroup.add_strict_left_mono" "REAL_LT_HALF2" > "HOL4Real.real.REAL_LT_HALF2" "REAL_LT_HALF1" > "NatSimprocs.half_gt_zero_iff" "REAL_LT_GT" > "HOL.order_less_not_sym" @@ -179,20 +179,20 @@ "REAL_LT_FRACTION" > "HOL4Real.real.REAL_LT_FRACTION" "REAL_LT_DIV" > "HOL4Real.real.REAL_LT_DIV" "REAL_LT_ANTISYM" > "HOL4Real.real.REAL_LT_ANTISYM" - "REAL_LT_ADD_SUB" > "Ring_and_Field.compare_rls_7" + "REAL_LT_ADD_SUB" > "OrderedGroup.compare_rls_7" "REAL_LT_ADDR" > "HOL4Real.real.REAL_LT_ADDR" "REAL_LT_ADDNEG2" > "HOL4Real.real.REAL_LT_ADDNEG2" "REAL_LT_ADDNEG" > "HOL4Real.real.REAL_LT_ADDNEG" "REAL_LT_ADDL" > "HOL4Real.real.REAL_LT_ADDL" - "REAL_LT_ADD2" > "Ring_and_Field.add_strict_mono" + "REAL_LT_ADD2" > "OrderedGroup.add_strict_mono" "REAL_LT_ADD1" > "HOL4Real.real.REAL_LT_ADD1" "REAL_LT_ADD" > "RealDef.real_add_order" "REAL_LT_1" > "HOL4Real.real.REAL_LT_1" - "REAL_LT_01" > "Ring_and_Field.ordered_semiring.zero_less_one" + "REAL_LT_01" > "Ring_and_Field.ordered_semidom.zero_less_one" "REAL_LTE_TRANS" > "Set.basic_trans_rules_24" "REAL_LTE_TOTAL" > "HOL4Real.real.REAL_LTE_TOTAL" "REAL_LTE_ANTSYM" > "HOL4Real.real.REAL_LTE_ANTSYM" - "REAL_LTE_ADD2" > "Ring_and_Field.add_less_le_mono" + "REAL_LTE_ADD2" > "OrderedGroup.add_less_le_mono" "REAL_LTE_ADD" > "HOL4Real.real.REAL_LTE_ADD" "REAL_LT1_POW2" > "HOL4Real.real.REAL_LT1_POW2" "REAL_LT" > "RealDef.real_of_nat_less_iff" @@ -200,46 +200,46 @@ "REAL_LINV_UNIQ" > "HOL4Real.real.REAL_LINV_UNIQ" "REAL_LE_TRANS" > "Set.basic_trans_rules_25" "REAL_LE_TOTAL" > "HOL.linorder.linorder_linear" - "REAL_LE_SUB_RADD" > "Ring_and_Field.compare_rls_8" - "REAL_LE_SUB_LADD" > "Ring_and_Field.compare_rls_9" + "REAL_LE_SUB_RADD" > "OrderedGroup.compare_rls_8" + "REAL_LE_SUB_LADD" > "OrderedGroup.compare_rls_9" "REAL_LE_SQUARE" > "Ring_and_Field.zero_le_square" - "REAL_LE_RNEG" > "HOL4Real.real.REAL_LE_RNEG" - "REAL_LE_RMUL_IMP" > "Ring_and_Field.mult_right_mono" + "REAL_LE_RNEG" > "OrderedGroup.le_eq_neg" + "REAL_LE_RMUL_IMP" > "Ring_and_Field.pordered_semiring.mult_right_mono" "REAL_LE_RMUL" > "RealDef.real_mult_le_cancel_iff1" "REAL_LE_REFL" > "HOL.order.order_refl" "REAL_LE_RDIV_EQ" > "Ring_and_Field.pos_le_divide_eq" "REAL_LE_RDIV" > "HOL4Real.real.REAL_LE_RDIV" - "REAL_LE_RADD" > "Ring_and_Field.add_le_cancel_right" + "REAL_LE_RADD" > "OrderedGroup.add_le_cancel_right" "REAL_LE_POW2" > "NatBin.zero_le_power2" "REAL_LE_NEGTOTAL" > "HOL4Real.real.REAL_LE_NEGTOTAL" - "REAL_LE_NEGR" > "Ring_and_Field.le_minus_self_iff" - "REAL_LE_NEGL" > "Ring_and_Field.minus_le_self_iff" - "REAL_LE_NEG2" > "Ring_and_Field.neg_le_iff_le" - "REAL_LE_NEG" > "Ring_and_Field.neg_le_iff_le" + "REAL_LE_NEGR" > "OrderedGroup.le_minus_self_iff" + "REAL_LE_NEGL" > "OrderedGroup.minus_le_self_iff" + "REAL_LE_NEG2" > "OrderedGroup.neg_le_iff_le" + "REAL_LE_NEG" > "OrderedGroup.neg_le_iff_le" "REAL_LE_MUL2" > "HOL4Real.real.REAL_LE_MUL2" - "REAL_LE_MUL" > "HOL4Real.real.REAL_LE_MUL" + "REAL_LE_MUL" > "Ring_and_Field.mult_pos_le" "REAL_LE_LT" > "HOL.order_le_less" "REAL_LE_LNEG" > "RealDef.real_0_le_add_iff" - "REAL_LE_LMUL_IMP" > "Ring_and_Field.mult_left_mono" + "REAL_LE_LMUL_IMP" > "Ring_and_Field.pordered_comm_semiring.mult_mono" "REAL_LE_LMUL" > "RealDef.real_mult_le_cancel_iff2" "REAL_LE_LDIV_EQ" > "Ring_and_Field.pos_divide_le_eq" "REAL_LE_LDIV" > "HOL4Real.real.REAL_LE_LDIV" - "REAL_LE_LADD_IMP" > "Ring_and_Field.almost_ordered_semiring.add_left_mono" - "REAL_LE_LADD" > "Ring_and_Field.add_le_cancel_left" + "REAL_LE_LADD_IMP" > "OrderedGroup.pordered_ab_semigroup_add.add_left_mono" + "REAL_LE_LADD" > "OrderedGroup.add_le_cancel_left" "REAL_LE_INV_EQ" > "Ring_and_Field.inverse_nonnegative_iff_nonnegative" "REAL_LE_INV" > "HOL4Real.real.REAL_LE_INV" - "REAL_LE_DOUBLE" > "HOL4Real.real.REAL_LE_DOUBLE" + "REAL_LE_DOUBLE" > "OrderedGroup.zero_le_double_add_iff_zero_le_single_add" "REAL_LE_DIV" > "HOL4Real.real.REAL_LE_DIV" "REAL_LE_ANTISYM" > "HOL.order_eq_iff" "REAL_LE_ADDR" > "HOL4Real.real.REAL_LE_ADDR" "REAL_LE_ADDL" > "HOL4Real.real.REAL_LE_ADDL" - "REAL_LE_ADD2" > "Ring_and_Field.add_mono" + "REAL_LE_ADD2" > "OrderedGroup.add_mono" "REAL_LE_ADD" > "RealDef.real_le_add_order" "REAL_LE_01" > "Ring_and_Field.zero_le_one" "REAL_LET_TRANS" > "Set.basic_trans_rules_23" "REAL_LET_TOTAL" > "HOL4Real.real.REAL_LET_TOTAL" "REAL_LET_ANTISYM" > "HOL4Real.real.REAL_LET_ANTISYM" - "REAL_LET_ADD2" > "Ring_and_Field.add_le_less_mono" + "REAL_LET_ADD2" > "OrderedGroup.add_le_less_mono" "REAL_LET_ADD" > "HOL4Real.real.REAL_LET_ADD" "REAL_LE1_POW2" > "HOL4Real.real.REAL_LE1_POW2" "REAL_LE" > "RealDef.real_of_nat_le_iff" @@ -262,14 +262,14 @@ "REAL_EQ_RMUL_IMP" > "Ring_and_Field.field_mult_cancel_right_lemma" "REAL_EQ_RMUL" > "Ring_and_Field.field_mult_cancel_right" "REAL_EQ_RDIV_EQ" > "HOL4Real.real.REAL_EQ_RDIV_EQ" - "REAL_EQ_RADD" > "Ring_and_Field.add_right_cancel" - "REAL_EQ_NEG" > "Ring_and_Field.neg_equal_iff_equal" + "REAL_EQ_RADD" > "OrderedGroup.add_right_cancel" + "REAL_EQ_NEG" > "OrderedGroup.neg_equal_iff_equal" "REAL_EQ_MUL_LCANCEL" > "Ring_and_Field.field_mult_cancel_left" "REAL_EQ_LMUL_IMP" > "HOL4Real.real.REAL_EQ_LMUL_IMP" "REAL_EQ_LMUL2" > "RealDef.real_mult_left_cancel" "REAL_EQ_LMUL" > "Ring_and_Field.field_mult_cancel_left" "REAL_EQ_LDIV_EQ" > "HOL4Real.real.REAL_EQ_LDIV_EQ" - "REAL_EQ_LADD" > "Ring_and_Field.add_left_cancel" + "REAL_EQ_LADD" > "OrderedGroup.add_left_cancel" "REAL_EQ_IMP_LE" > "HOL.order_eq_refl" "REAL_ENTIRE" > "Ring_and_Field.field_mult_eq_0_iff" "REAL_DOWN2" > "RealDef.real_lbound_gt_zero" @@ -285,22 +285,22 @@ "REAL_ARCH" > "RComplete.reals_Archimedean3" "REAL_ADD_SYM" > "Ring_and_Field.ring_eq_simps_9" "REAL_ADD_SUB2" > "HOL4Real.real.REAL_ADD_SUB2" - "REAL_ADD_SUB" > "Ring_and_Field.add_minus_self_right" - "REAL_ADD_RINV" > "Ring_and_Field.right_minus" + "REAL_ADD_SUB" > "HOL4Real.real.REAL_ADD_SUB" + "REAL_ADD_RINV" > "OrderedGroup.right_minus" "REAL_ADD_RID_UNIQ" > "HOL4Real.real.REAL_ADD_RID_UNIQ" - "REAL_ADD_RID" > "Ring_and_Field.add_0_right" + "REAL_ADD_RID" > "OrderedGroup.add_0_right" "REAL_ADD_RDISTRIB" > "Ring_and_Field.ring_eq_simps_4" "REAL_ADD_LINV" > "HOL4Compat.REAL_ADD_LINV" "REAL_ADD_LID_UNIQ" > "HOL4Real.real.REAL_ADD_LID_UNIQ" - "REAL_ADD_LID" > "Ring_and_Field.abelian_semigroup.add_0" + "REAL_ADD_LID" > "OrderedGroup.comm_monoid_add.add_0" "REAL_ADD_LDISTRIB" > "Ring_and_Field.ring_eq_simps_5" "REAL_ADD_ASSOC" > "HOL4Compat.REAL_ADD_ASSOC" "REAL_ADD2_SUB2" > "HOL4Real.real.REAL_ADD2_SUB2" "REAL_ADD" > "RealDef.real_of_nat_add" - "REAL_ABS_TRIANGLE" > "Ring_and_Field.abs_triangle_ineq" - "REAL_ABS_POS" > "Ring_and_Field.abs_ge_zero" + "REAL_ABS_TRIANGLE" > "OrderedGroup.abs_triangle_ineq" + "REAL_ABS_POS" > "OrderedGroup.abs_ge_zero" "REAL_ABS_MUL" > "Ring_and_Field.abs_mult" - "REAL_ABS_0" > "Ring_and_Field.abs_zero" + "REAL_ABS_0" > "OrderedGroup.abs_zero" "REAL_10" > "HOL4Compat.REAL_10" "REAL_1" > "HOL4Real.real.REAL_1" "REAL_0" > "HOL4Real.real.REAL_0" @@ -326,8 +326,8 @@ "POW_2" > "NatBin.power2_eq_square" "POW_1" > "Power.power_one_right" "POW_0" > "Power.power_0_Suc" - "ABS_ZERO" > "Ring_and_Field.abs_zero_iff" - "ABS_TRIANGLE" > "Ring_and_Field.abs_triangle_ineq" + "ABS_ZERO" > "OrderedGroup.abs_eq_0" + "ABS_TRIANGLE" > "OrderedGroup.abs_triangle_ineq" "ABS_SUM" > "HOL4Real.real.ABS_SUM" "ABS_SUB_ABS" > "HOL4Real.real.ABS_SUB_ABS" "ABS_SUB" > "HOL4Real.real.ABS_SUB" @@ -336,13 +336,13 @@ "ABS_SIGN" > "HOL4Real.real.ABS_SIGN" "ABS_REFL" > "HOL4Real.real.ABS_REFL" "ABS_POW2" > "NatBin.abs_power2" - "ABS_POS" > "Ring_and_Field.abs_ge_zero" - "ABS_NZ" > "Ring_and_Field.zero_less_abs_iff" - "ABS_NEG" > "Ring_and_Field.abs_minus_cancel" + "ABS_POS" > "OrderedGroup.abs_ge_zero" + "ABS_NZ" > "OrderedGroup.zero_less_abs_iff" + "ABS_NEG" > "OrderedGroup.abs_minus_cancel" "ABS_N" > "RealDef.abs_real_of_nat_cancel" "ABS_MUL" > "Ring_and_Field.abs_mult" "ABS_LT_MUL2" > "HOL4Real.real.ABS_LT_MUL2" - "ABS_LE" > "Ring_and_Field.abs_ge_self" + "ABS_LE" > "OrderedGroup.abs_ge_self" "ABS_INV" > "Ring_and_Field.nonzero_abs_inverse" "ABS_DIV" > "Ring_and_Field.nonzero_abs_divide" "ABS_CIRCLE" > "HOL4Real.real.ABS_CIRCLE" @@ -352,8 +352,8 @@ "ABS_BETWEEN2" > "HOL4Real.real.ABS_BETWEEN2" "ABS_BETWEEN1" > "HOL4Real.real.ABS_BETWEEN1" "ABS_BETWEEN" > "HOL4Real.real.ABS_BETWEEN" - "ABS_ABS" > "Ring_and_Field.abs_idempotent" + "ABS_ABS" > "OrderedGroup.abs_idempotent" "ABS_1" > "Ring_and_Field.abs_one" - "ABS_0" > "Ring_and_Field.abs_zero" + "ABS_0" > "OrderedGroup.abs_zero" end diff -r b702848de41f -r 1e83aa391ade src/HOL/Import/HOL/realax.imp --- a/src/HOL/Import/HOL/realax.imp Fri May 21 21:28:58 2004 +0200 +++ b/src/HOL/Import/HOL/realax.imp Fri May 21 21:42:05 2004 +0200 @@ -93,18 +93,18 @@ "REAL_SUP_ALLPOS" > "HOL4Compat.REAL_SUP_ALLPOS" "REAL_MUL_SYM" > "Ring_and_Field.ring_eq_simps_2" "REAL_MUL_LINV" > "HOL4Compat.REAL_MUL_LINV" - "REAL_MUL_LID" > "Ring_and_Field.almost_semiring.mult_1" + "REAL_MUL_LID" > "OrderedGroup.comm_monoid_mult.mult_1" "REAL_MUL_ASSOC" > "HOL4Compat.REAL_MUL_ASSOC" "REAL_LT_TRANS" > "Set.basic_trans_rules_21" "REAL_LT_TOTAL" > "HOL4Compat.REAL_LT_TOTAL" "REAL_LT_REFL" > "HOL.order_less_irrefl" "REAL_LT_MUL" > "Ring_and_Field.mult_pos" - "REAL_LT_IADD" > "Ring_and_Field.add_strict_left_mono" + "REAL_LT_IADD" > "OrderedGroup.add_strict_left_mono" "REAL_LDISTRIB" > "Ring_and_Field.ring_eq_simps_5" "REAL_INV_0" > "Ring_and_Field.division_by_zero.inverse_zero" "REAL_ADD_SYM" > "Ring_and_Field.ring_eq_simps_9" "REAL_ADD_LINV" > "HOL4Compat.REAL_ADD_LINV" - "REAL_ADD_LID" > "Ring_and_Field.abelian_semigroup.add_0" + "REAL_ADD_LID" > "OrderedGroup.comm_monoid_add.add_0" "REAL_ADD_ASSOC" > "HOL4Compat.REAL_ADD_ASSOC" "REAL_10" > "HOL4Compat.REAL_10" "HREAL_RDISTRIB" > "HOL4Real.realax.HREAL_RDISTRIB"