# HG changeset patch
# User wenzelm
# Date 1183487168 -7200
# Node ID 84f0996a530bfc69ddc83522a1bf63acd1388945
# Parent  d4f1d6ef119cf32d34a9c38b0bdd0bcc1cf35f25
rename class dom to ring_1_no_zero_divisors (cf. HOL/Ring_and_Field.thy 1.84 by huffman);

diff -r d4f1d6ef119c -r 84f0996a530b src/HOL/Hyperreal/StarClasses.thy
--- a/src/HOL/Hyperreal/StarClasses.thy	Tue Jul 03 18:42:09 2007 +0200
+++ b/src/HOL/Hyperreal/StarClasses.thy	Tue Jul 03 20:26:08 2007 +0200
@@ -365,7 +365,7 @@
 instance star :: (ring_1) ring_1 ..
 instance star :: (comm_ring_1) comm_ring_1 ..
 instance star :: (ring_no_zero_divisors) ring_no_zero_divisors ..
-instance star :: (dom) dom ..
+instance star :: (ring_1_no_zero_divisors) ring_1_no_zero_divisors ..
 instance star :: (idom) idom .. 
 
 instance star :: (division_ring) division_ring