Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Import/HOL/realax.imp
changeset 14620 1be590fd2422
parent 14516 a183dec876ab
child 14796 1e83aa391ade 
--- 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"
isabelle