src/HOL/Import/HOL/realax.imp
changeset 17188 a26a4fc323ed
parent 16775 c1b87ef4a1c3
child 17644 bd59bfd4bf37
--- a/src/HOL/Import/HOL/realax.imp	Mon Aug 29 16:25:24 2005 +0200
+++ b/src/HOL/Import/HOL/realax.imp	Mon Aug 29 16:51:39 2005 +0200
@@ -91,9 +91,9 @@
   "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.ring_eq_simps_6"
+  "REAL_MUL_SYM" > "IntDef.zmult_ac_2"
   "REAL_MUL_LINV" > "HOL4Compat.REAL_MUL_LINV"
-  "REAL_MUL_LID" > "OrderedGroup.comm_monoid_mult.mult_1"
+  "REAL_MUL_LID" > "Finite_Set.AC_mult.f_e.left_ident"
   "REAL_MUL_ASSOC" > "HOL4Compat.REAL_MUL_ASSOC"
   "REAL_LT_TRANS" > "Set.basic_trans_rules_21"
   "REAL_LT_TOTAL" > "HOL4Compat.REAL_LT_TOTAL"
@@ -102,9 +102,9 @@
   "REAL_LT_IADD" > "OrderedGroup.add_strict_left_mono"
   "REAL_LDISTRIB" > "Ring_and_Field.ring_eq_simps_2"
   "REAL_INV_0" > "Ring_and_Field.division_by_zero.inverse_zero"
-  "REAL_ADD_SYM" > "Ring_and_Field.ring_eq_simps_9"
+  "REAL_ADD_SYM" > "Finite_Set.AC_add.f.AC_2"
   "REAL_ADD_LINV" > "HOL4Compat.REAL_ADD_LINV"
-  "REAL_ADD_LID" > "OrderedGroup.comm_monoid_add.add_0"
+  "REAL_ADD_LID" > "Finite_Set.AC_add.f_e.left_ident"
   "REAL_ADD_ASSOC" > "HOL4Compat.REAL_ADD_ASSOC"
   "REAL_10" > "HOL4Compat.REAL_10"
   "HREAL_RDISTRIB" > "HOL4Real.realax.HREAL_RDISTRIB"