--- a/src/HOL/Import/HOL/real.imp Sat Apr 17 20:04:23 2004 +0200
+++ b/src/HOL/Import/HOL/real.imp Sat Apr 17 23:53:35 2004 +0200
@@ -77,13 +77,13 @@
"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_RDISTRIB" > "Ring_and_Field.left_diff_distrib"
+ "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_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.right_diff_distrib"
+ "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"
@@ -91,7 +91,7 @@
"REAL_SUB_0" > "Ring_and_Field.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_distrib_2"
+ "REAL_RDISTRIB" > "Ring_and_Field.ring_eq_simps_4"
"REAL_POW_POW" > "Power.power_mult"
"REAL_POW_MONO_LT" > "Power.power_strict_increasing"
"REAL_POW_LT2" > "HOL4Real.real.REAL_POW_LT2"
@@ -129,7 +129,7 @@
"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_MUL_SYM" > "Ring_and_Field.mult_ac_2"
+ "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"
@@ -243,7 +243,7 @@
"REAL_LET_ADD" > "HOL4Real.real.REAL_LET_ADD"
"REAL_LE1_POW2" > "HOL4Real.real.REAL_LE1_POW2"
"REAL_LE" > "RealDef.real_of_nat_le_iff"
- "REAL_LDISTRIB" > "Ring_and_Field.ring_distrib_1"
+ "REAL_LDISTRIB" > "Ring_and_Field.ring_eq_simps_5"
"REAL_INV_POS" > "Ring_and_Field.positive_imp_inverse_positive"
"REAL_INV_NZ" > "Ring_and_Field.nonzero_imp_inverse_nonzero"
"REAL_INV_MUL" > "HOL4Real.real.REAL_INV_MUL"
@@ -257,8 +257,8 @@
"REAL_INJ" > "RealDef.real_of_nat_inject"
"REAL_HALF_DOUBLE" > "RComplete.real_sum_of_halves"
"REAL_FACT_NZ" > "HOL4Real.real.REAL_FACT_NZ"
- "REAL_EQ_SUB_RADD" > "Ring_and_Field.compare_rls_10"
- "REAL_EQ_SUB_LADD" > "Ring_and_Field.compare_rls_11"
+ "REAL_EQ_SUB_RADD" > "Ring_and_Field.ring_eq_simps_15"
+ "REAL_EQ_SUB_LADD" > "Ring_and_Field.ring_eq_simps_16"
"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"
@@ -283,17 +283,17 @@
"REAL_DIFFSQ" > "HOL4Real.real.REAL_DIFFSQ"
"REAL_ARCH_LEAST" > "HOL4Real.real.REAL_ARCH_LEAST"
"REAL_ARCH" > "RComplete.reals_Archimedean3"
- "REAL_ADD_SYM" > "Ring_and_Field.add_ac_2"
+ "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_RID_UNIQ" > "HOL4Real.real.REAL_ADD_RID_UNIQ"
"REAL_ADD_RID" > "Ring_and_Field.add_0_right"
- "REAL_ADD_RDISTRIB" > "Ring_and_Field.ring_distrib_2"
+ "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_LDISTRIB" > "Ring_and_Field.ring_distrib_1"
+ "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"