1.1 --- a/src/HOL/Integ/IntArith.thy	Tue May 11 14:00:02 2004 +0200
     1.2 +++ b/src/HOL/Integ/IntArith.thy	Tue May 11 20:11:08 2004 +0200
     1.3 @@ -126,11 +126,11 @@
     1.4    finally show ?thesis .
     1.5  qed
     1.6  
     1.7 -lemma abs_minus_one [simp]: "abs (-1) = (1::'a::{ordered_ring,number_ring})"
     1.8 +lemma abs_minus_one [simp]: "abs (-1) = (1::'a::{ordered_idom,number_ring})"
     1.9  by (simp add: abs_if)
    1.10  
    1.11  lemma abs_power_minus_one [simp]:
    1.12 -     "abs(-1 ^ n) = (1::'a::{ordered_ring,number_ring,ringpower})"
    1.13 +     "abs(-1 ^ n) = (1::'a::{ordered_idom,number_ring,ringpower})"
    1.14  by (simp add: power_abs)
    1.15  
    1.16  lemma of_int_number_of_eq: