1.1 --- a/src/HOL/Integ/int_arith1.ML	Tue May 11 14:00:02 2004 +0200
     1.2 +++ b/src/HOL/Integ/int_arith1.ML	Tue May 11 20:11:08 2004 +0200
     1.3 @@ -383,20 +383,20 @@
     1.4        "(l::'a::number_ring) = m * n"],
     1.5       EqCancelNumerals.proc),
     1.6      ("intless_cancel_numerals",
     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_ring,number_ring}) - m < n",
    1.10 -      "(l::'a::{ordered_ring,number_ring}) < m - n",
    1.11 -      "(l::'a::{ordered_ring,number_ring}) * m < n",
    1.12 -      "(l::'a::{ordered_ring,number_ring}) < m * n"],
    1.13 +     ["(l::'a::{ordered_idom,number_ring}) + m < n",
    1.14 +      "(l::'a::{ordered_idom,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 +      "(l::'a::{ordered_idom,number_ring}) * m < n",
    1.18 +      "(l::'a::{ordered_idom,number_ring}) < m * n"],
    1.19       LessCancelNumerals.proc),
    1.20      ("intle_cancel_numerals",
    1.21 -     ["(l::'a::{ordered_ring,number_ring}) + m <= n",
    1.22 -      "(l::'a::{ordered_ring,number_ring}) <= m + n",
    1.23 -      "(l::'a::{ordered_ring,number_ring}) - m <= n",
    1.24 -      "(l::'a::{ordered_ring,number_ring}) <= m - n",
    1.25 -      "(l::'a::{ordered_ring,number_ring}) * m <= n",
    1.26 -      "(l::'a::{ordered_ring,number_ring}) <= m * n"],
    1.27 +     ["(l::'a::{ordered_idom,number_ring}) + m <= n",
    1.28 +      "(l::'a::{ordered_idom,number_ring}) <= m + n",
    1.29 +      "(l::'a::{ordered_idom,number_ring}) - m <= n",
    1.30 +      "(l::'a::{ordered_idom,number_ring}) <= m - n",
    1.31 +      "(l::'a::{ordered_idom,number_ring}) * m <= n",
    1.32 +      "(l::'a::{ordered_idom,number_ring}) <= m * n"],
    1.33       LeCancelNumerals.proc)];
    1.34  
    1.35  
    1.36 @@ -488,7 +488,7 @@
    1.37  
    1.38  val assoc_fold_simproc =
    1.39    Bin_Simprocs.prep_simproc
    1.40 -   ("semiring_assoc_fold", ["(a::'a::semiring) * b"],
    1.41 +   ("semiring_assoc_fold", ["(a::'a::comm_semiring_1_cancel) * b"],
    1.42      Semiring_Times_Assoc.proc);
    1.43  
    1.44  Addsimprocs [assoc_fold_simproc];
    1.45 @@ -545,9 +545,9 @@
    1.46  val fast_int_arith_simproc =
    1.47    Simplifier.simproc (Theory.sign_of (the_context()))
    1.48    "fast_int_arith" 
    1.49 -     ["(m::'a::{ordered_ring,number_ring}) < n",
    1.50 -      "(m::'a::{ordered_ring,number_ring}) <= n",
    1.51 -      "(m::'a::{ordered_ring,number_ring}) = n"] Fast_Arith.lin_arith_prover;
    1.52 +     ["(m::'a::{ordered_idom,number_ring}) < n",
    1.53 +      "(m::'a::{ordered_idom,number_ring}) <= n",
    1.54 +      "(m::'a::{ordered_idom,number_ring}) = n"] Fast_Arith.lin_arith_prover;
    1.55  
    1.56  Addsimprocs [fast_int_arith_simproc]
    1.57