src/HOL/Tools/numeral_simprocs.ML

       "(l::'a::number_ring) = m - n",
       "(l::'a::number_ring) * m = n",
       "(l::'a::number_ring) = m * n"],
      K EqCancelNumerals.proc),
     ("intless_cancel_numerals",
-     ["(l::'a::{ordered_idom,number_ring}) + m < n",
-      "(l::'a::{ordered_idom,number_ring}) < m + n",
-      "(l::'a::{ordered_idom,number_ring}) - m < n",
-      "(l::'a::{ordered_idom,number_ring}) < m - n",
-      "(l::'a::{ordered_idom,number_ring}) * m < n",
-      "(l::'a::{ordered_idom,number_ring}) < m * n"],
+     ["(l::'a::{linordered_idom,number_ring}) + m < n",
+      "(l::'a::{linordered_idom,number_ring}) < m + n",
+      "(l::'a::{linordered_idom,number_ring}) - m < n",
+      "(l::'a::{linordered_idom,number_ring}) < m - n",
+      "(l::'a::{linordered_idom,number_ring}) * m < n",
+      "(l::'a::{linordered_idom,number_ring}) < m * n"],
      K LessCancelNumerals.proc),
     ("intle_cancel_numerals",
-     ["(l::'a::{ordered_idom,number_ring}) + m <= n",
-      "(l::'a::{ordered_idom,number_ring}) <= m + n",
-      "(l::'a::{ordered_idom,number_ring}) - m <= n",
-      "(l::'a::{ordered_idom,number_ring}) <= m - n",
-      "(l::'a::{ordered_idom,number_ring}) * m <= n",
-      "(l::'a::{ordered_idom,number_ring}) <= m * n"],
+     ["(l::'a::{linordered_idom,number_ring}) + m <= n",
+      "(l::'a::{linordered_idom,number_ring}) <= m + n",
+      "(l::'a::{linordered_idom,number_ring}) - m <= n",
+      "(l::'a::{linordered_idom,number_ring}) <= m - n",
+      "(l::'a::{linordered_idom,number_ring}) * m <= n",
+      "(l::'a::{linordered_idom,number_ring}) <= m * n"],
      K LeCancelNumerals.proc)];
 
 structure CombineNumeralsData =
   struct
   type coeff            = int

    [("ring_eq_cancel_numeral_factor",
      ["(l::'a::{idom,number_ring}) * m = n",
       "(l::'a::{idom,number_ring}) = m * n"],
      K EqCancelNumeralFactor.proc),
     ("ring_less_cancel_numeral_factor",
-     ["(l::'a::{ordered_idom,number_ring}) * m < n",
-      "(l::'a::{ordered_idom,number_ring}) < m * n"],
+     ["(l::'a::{linordered_idom,number_ring}) * m < n",
+      "(l::'a::{linordered_idom,number_ring}) < m * n"],
      K LessCancelNumeralFactor.proc),
     ("ring_le_cancel_numeral_factor",
-     ["(l::'a::{ordered_idom,number_ring}) * m <= n",
-      "(l::'a::{ordered_idom,number_ring}) <= m * n"],
+     ["(l::'a::{linordered_idom,number_ring}) * m <= n",
+      "(l::'a::{linordered_idom,number_ring}) <= m * n"],
      K LeCancelNumeralFactor.proc),
     ("int_div_cancel_numeral_factors",
      ["((l::'a::{semiring_div,number_ring}) * m) div n",
       "(l::'a::{semiring_div,number_ring}) div (m * n)"],
      K DivCancelNumeralFactor.proc),

   map (Arith_Data.prep_simproc @{theory})
    [("ring_eq_cancel_factor",
      ["(l::'a::idom) * m = n",
       "(l::'a::idom) = m * n"],
      K EqCancelFactor.proc),
-    ("ordered_ring_le_cancel_factor",
-     ["(l::'a::ordered_ring) * m <= n",
-      "(l::'a::ordered_ring) <= m * n"],
+    ("linlinordered_ring_le_cancel_factor",
+     ["(l::'a::linordered_ring) * m <= n",
+      "(l::'a::linordered_ring) <= m * n"],
      K LeCancelFactor.proc),
-    ("ordered_ring_less_cancel_factor",
-     ["(l::'a::ordered_ring) * m < n",
-      "(l::'a::ordered_ring) < m * n"],
+    ("linlinordered_ring_less_cancel_factor",
+     ["(l::'a::linordered_ring) * m < n",
+      "(l::'a::linordered_ring) < m * n"],
      K LessCancelFactor.proc),
     ("int_div_cancel_factor",
      ["((l::'a::semiring_div) * m) div n", "(l::'a::semiring_div) div (m * n)"],
      K DivCancelFactor.proc),
     ("int_mod_cancel_factor",