1.1 --- a/src/HOL/arith_data.ML	Tue May 11 14:00:02 2004 +0200
     1.2 +++ b/src/HOL/arith_data.ML	Tue May 11 20:11:08 2004 +0200
     1.3 @@ -386,10 +386,10 @@
     1.4  val add_mono_thms_ordered_semiring = map (fn s => prove_goal (the_context ()) s
     1.5   (fn prems => [cut_facts_tac prems 1,
     1.6                 blast_tac (claset() addIs [add_mono]) 1]))
     1.7 -["(i <= j) & (k <= l) ==> i + k <= j + (l::'a::ordered_semiring)",
     1.8 - "(i  = j) & (k <= l) ==> i + k <= j + (l::'a::ordered_semiring)",
     1.9 - "(i <= j) & (k  = l) ==> i + k <= j + (l::'a::ordered_semiring)",
    1.10 - "(i  = j) & (k  = l) ==> i + k  = j + (l::'a::ordered_semiring)"
    1.11 +["(i <= j) & (k <= l) ==> i + k <= j + (l::'a::ordered_semidom)",
    1.12 + "(i  = j) & (k <= l) ==> i + k <= j + (l::'a::ordered_semidom)",
    1.13 + "(i <= j) & (k  = l) ==> i + k <= j + (l::'a::ordered_semidom)",
    1.14 + "(i  = j) & (k  = l) ==> i + k  = j + (l::'a::ordered_semidom)"
    1.15  ];
    1.16  
    1.17  in