# HG changeset patch
# User huffman
# Date 1183476516 -7200
# Node ID 4b4165cb3e0d220e8442651dcaadbf458b9c9227
# Parent  12271cfad085b9cd86e6a249018dfbd79196d654
rename class dom to ring_1_no_zero_divisors

diff -r 12271cfad085 -r 4b4165cb3e0d src/HOL/Power.thy
--- 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:
diff -r 12271cfad085 -r 4b4165cb3e0d src/HOL/Ring_and_Field.thy
--- a/src/HOL/Ring_and_Field.thy	Tue Jul 03 17:17:17 2007 +0200
+++ b/src/HOL/Ring_and_Field.thy	Tue Jul 03 17:28:36 2007 +0200
@@ -124,18 +124,17 @@
 
 class ring_no_zero_divisors = ring + no_zero_divisors
 
-class dom = ring_1 + ring_no_zero_divisors
-hide const dom
+class ring_1_no_zero_divisors = ring_1 + ring_no_zero_divisors
 
 class idom = comm_ring_1 + no_zero_divisors
 
-instance idom \<subseteq> dom ..
+instance idom \<subseteq> ring_1_no_zero_divisors ..
 
 class division_ring = ring_1 + inverse +
   assumes left_inverse [simp]:  "a \<noteq> \<^loc>0 \<Longrightarrow> inverse a \<^loc>* a = \<^loc>1"
   assumes right_inverse [simp]: "a \<noteq> \<^loc>0 \<Longrightarrow> a \<^loc>* inverse a = \<^loc>1"
 
-instance division_ring \<subseteq> dom
+instance division_ring \<subseteq> ring_1_no_zero_divisors
 proof
   fix a b :: 'a
   assume a: "a \<noteq> 0" and b: "b \<noteq> 0"
@@ -717,22 +716,22 @@
 by (insert mult_less_cancel_left [of c a 1], simp)
 
 lemma mult_cancel_right1 [simp]:
-  fixes c :: "'a :: dom"
+  fixes c :: "'a :: ring_1_no_zero_divisors"
   shows "(c = b*c) = (c = 0 | b=1)"
 by (insert mult_cancel_right [of 1 c b], force)
 
 lemma mult_cancel_right2 [simp]:
-  fixes c :: "'a :: dom"
+  fixes c :: "'a :: ring_1_no_zero_divisors"
   shows "(a*c = c) = (c = 0 | a=1)"
 by (insert mult_cancel_right [of a c 1], simp)
  
 lemma mult_cancel_left1 [simp]:
-  fixes c :: "'a :: dom"
+  fixes c :: "'a :: ring_1_no_zero_divisors"
   shows "(c = c*b) = (c = 0 | b=1)"
 by (insert mult_cancel_left [of c 1 b], force)
 
 lemma mult_cancel_left2 [simp]:
-  fixes c :: "'a :: dom"
+  fixes c :: "'a :: ring_1_no_zero_divisors"
   shows "(c*a = c) = (c = 0 | a=1)"
 by (insert mult_cancel_left [of c a 1], simp)