1.1 --- a/src/HOL/Integ/Parity.thy	Tue May 11 14:00:02 2004 +0200
     1.2 +++ b/src/HOL/Integ/Parity.thy	Tue May 11 20:11:08 2004 +0200
     1.3 @@ -249,7 +249,7 @@
     1.4    by (rule neg_one_even_odd_power [THEN conjunct2, THEN mp], assumption)
     1.5  
     1.6  lemma neg_power_if:
     1.7 -     "(-x::'a::{ring,ringpower}) ^ n = 
     1.8 +     "(-x::'a::{comm_ring_1,ringpower}) ^ n = 
     1.9        (if even n then (x ^ n) else -(x ^ n))"
    1.10    by (induct n, simp_all split: split_if_asm add: power_Suc) 
    1.11  
    1.12 @@ -257,13 +257,13 @@
    1.13  subsection {* An Equivalence for @{term "0 \<le> a^n"} *}
    1.14  
    1.15  lemma even_power_le_0_imp_0:
    1.16 -     "a ^ (2*k) \<le> (0::'a::{ordered_ring,ringpower}) ==> a=0"
    1.17 +     "a ^ (2*k) \<le> (0::'a::{ordered_idom,ringpower}) ==> a=0"
    1.18  apply (induct k) 
    1.19  apply (auto simp add: zero_le_mult_iff mult_le_0_iff power_Suc)  
    1.20  done
    1.21  
    1.22  lemma zero_le_power_iff:
    1.23 -     "(0 \<le> a^n) = (0 \<le> (a::'a::{ordered_ring,ringpower}) | even n)"
    1.24 +     "(0 \<le> a^n) = (0 \<le> (a::'a::{ordered_idom,ringpower}) | even n)"
    1.25        (is "?P n")
    1.26  proof cases
    1.27    assume even: "even n"