diff -r 8876ad83b1fb -r 1be590fd2422 src/HOL/Import/HOL/realax.imp
--- a/src/HOL/Import/HOL/realax.imp	Sat Apr 17 20:04:23 2004 +0200
+++ b/src/HOL/Import/HOL/realax.imp	Sat Apr 17 23:53:35 2004 +0200
@@ -91,7 +91,7 @@
   "TREAL_ADD_ASSOC" > "HOL4Real.realax.TREAL_ADD_ASSOC"
   "TREAL_10" > "HOL4Real.realax.TREAL_10"
   "REAL_SUP_ALLPOS" > "HOL4Compat.REAL_SUP_ALLPOS"
-  "REAL_MUL_SYM" > "Ring_and_Field.mult_ac_2"
+  "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_ASSOC" > "HOL4Compat.REAL_MUL_ASSOC"
@@ -100,9 +100,9 @@
   "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_LDISTRIB" > "Ring_and_Field.ring_distrib_1"
+  "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.add_ac_2"
+  "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_ASSOC" > "HOL4Compat.REAL_ADD_ASSOC"