# HG changeset patch
# User huffman
# Date 1179422979 -7200
# Node ID fc54d5fc4a7a77065849147f22434daa42dde943
# Parent  b9e2a133e84e1606f02218465da57e57f093ef45
add classes ring_no_zero_divisors and dom

diff -r b9e2a133e84e -r fc54d5fc4a7a src/HOL/Hyperreal/StarClasses.thy
--- a/src/HOL/Hyperreal/StarClasses.thy	Thu May 17 19:12:47 2007 +0200
+++ b/src/HOL/Hyperreal/StarClasses.thy	Thu May 17 19:29:39 2007 +0200
@@ -364,6 +364,8 @@
 instance star :: (comm_ring) comm_ring ..
 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 :: (idom) idom .. 
 
 instance star :: (division_ring) division_ring