1.1 --- a/src/HOL/Power.thy	Tue Jul 03 17:17:17 2007 +0200
     1.2 +++ b/src/HOL/Power.thy	Tue Jul 03 17:28:36 2007 +0200
     1.3 @@ -133,7 +133,7 @@
     1.4  done
     1.5  
     1.6  lemma power_eq_0_iff [simp]:
     1.7 -     "(a^n = 0) = (a = (0::'a::{dom,recpower}) & 0<n)"
     1.8 +     "(a^n = 0) = (a = (0::'a::{ring_1_no_zero_divisors,recpower}) & 0<n)"
     1.9  apply (induct "n")
    1.10  apply (auto simp add: power_Suc zero_neq_one [THEN not_sym])
    1.11  done
    1.12 @@ -142,7 +142,7 @@
    1.13       "(a^n = 0) = (a = (0::'a::{division_ring,recpower}) & 0<n)"
    1.14  by simp (* TODO: delete *)
    1.15  
    1.16 -lemma field_power_not_zero: "a \<noteq> (0::'a::{dom,recpower}) ==> a^n \<noteq> 0"
    1.17 +lemma field_power_not_zero: "a \<noteq> (0::'a::{ring_1_no_zero_divisors,recpower}) ==> a^n \<noteq> 0"
    1.18  by force
    1.19  
    1.20  lemma nonzero_power_inverse: