--- 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"