1.1 --- a/src/HOL/Integ/int_factor_simprocs.ML	Tue May 11 14:00:02 2004 +0200
     1.2 +++ b/src/HOL/Integ/int_factor_simprocs.ML	Tue May 11 20:11:08 2004 +0200
     1.3 @@ -116,16 +116,16 @@
     1.4  val ring_cancel_numeral_factors =
     1.5    map Bin_Simprocs.prep_simproc
     1.6     [("ring_eq_cancel_numeral_factor",
     1.7 -     ["(l::'a::{ordered_ring,number_ring}) * m = n",
     1.8 -      "(l::'a::{ordered_ring,number_ring}) = m * n"],
     1.9 +     ["(l::'a::{ordered_idom,number_ring}) * m = n",
    1.10 +      "(l::'a::{ordered_idom,number_ring}) = m * n"],
    1.11       EqCancelNumeralFactor.proc),
    1.12      ("ring_less_cancel_numeral_factor",
    1.13 -     ["(l::'a::{ordered_ring,number_ring}) * m < n",
    1.14 -      "(l::'a::{ordered_ring,number_ring}) < m * n"],
    1.15 +     ["(l::'a::{ordered_idom,number_ring}) * m < n",
    1.16 +      "(l::'a::{ordered_idom,number_ring}) < m * n"],
    1.17       LessCancelNumeralFactor.proc),
    1.18      ("ring_le_cancel_numeral_factor",
    1.19 -     ["(l::'a::{ordered_ring,number_ring}) * m <= n",
    1.20 -      "(l::'a::{ordered_ring,number_ring}) <= m * n"],
    1.21 +     ["(l::'a::{ordered_idom,number_ring}) * m <= n",
    1.22 +      "(l::'a::{ordered_idom,number_ring}) <= m * n"],
    1.23       LeCancelNumeralFactor.proc),
    1.24      ("int_div_cancel_numeral_factors",
    1.25       ["((l::int) * m) div n", "(l::int) div (m * n)"],
    1.26 @@ -249,7 +249,7 @@
    1.27    val norm_tac = ALLGOALS (simp_tac (HOL_ss addsimps mult_1s@mult_ac))
    1.28    end;
    1.29  
    1.30 -(*mult_cancel_left requires an ordered ring, such as int. The version in
    1.31 +(*mult_cancel_left requires an ordered comm_ring_1, such as int. The version in
    1.32    rat_arith.ML works for all fields.*)
    1.33  structure EqCancelFactor = ExtractCommonTermFun
    1.34   (open CancelFactorCommon