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/Tools/numeral_simprocs.ML
changeset 35043 07dbdf60d5ad
parent 35030 f2f1e50bf65d
child 35050 9f841f20dca6 
--- a/src/HOL/Tools/numeral_simprocs.ML	Mon Feb 08 14:22:22 2010 +0100
+++ b/src/HOL/Tools/numeral_simprocs.ML	Mon Feb 08 14:22:22 2010 +0100
@@ -581,11 +581,11 @@
      ["(l::'a::idom) * m = n",
       "(l::'a::idom) = m * n"],
      K EqCancelFactor.proc),
-    ("linlinordered_ring_le_cancel_factor",
+    ("linordered_ring_le_cancel_factor",
      ["(l::'a::linordered_ring) * m <= n",
       "(l::'a::linordered_ring) <= m * n"],
      K LeCancelFactor.proc),
-    ("linlinordered_ring_less_cancel_factor",
+    ("linordered_ring_less_cancel_factor",
      ["(l::'a::linordered_ring) * m < n",
       "(l::'a::linordered_ring) < m * n"],
      K LessCancelFactor.proc),
isabelle