--- a/src/HOL/Power.thy Tue Jul 03 17:17:17 2007 +0200
+++ b/src/HOL/Power.thy Tue Jul 03 17:28:36 2007 +0200
@@ -133,7 +133,7 @@
done
lemma power_eq_0_iff [simp]:
- "(a^n = 0) = (a = (0::'a::{dom,recpower}) & 0<n)"
+ "(a^n = 0) = (a = (0::'a::{ring_1_no_zero_divisors,recpower}) & 0<n)"
apply (induct "n")
apply (auto simp add: power_Suc zero_neq_one [THEN not_sym])
done
@@ -142,7 +142,7 @@
"(a^n = 0) = (a = (0::'a::{division_ring,recpower}) & 0<n)"
by simp (* TODO: delete *)
-lemma field_power_not_zero: "a \<noteq> (0::'a::{dom,recpower}) ==> a^n \<noteq> 0"
+lemma field_power_not_zero: "a \<noteq> (0::'a::{ring_1_no_zero_divisors,recpower}) ==> a^n \<noteq> 0"
by force
lemma nonzero_power_inverse: