| changeset 23551 | 84f0996a530b |
| parent 23282 | dfc459989d24 |
| child 23879 | 4776af8be741 |
--- 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