--- a/src/HOL/Tools/numeral_simprocs.ML Mon Feb 08 11:01:47 2010 +0100
+++ b/src/HOL/Tools/numeral_simprocs.ML Mon Feb 08 11:13:30 2010 +0100
@@ -255,20 +255,20 @@
"(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 =
@@ -431,12 +431,12 @@
"(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",
@@ -581,13 +581,13 @@
["(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)"],