a ring_div is a ring_1_no_zero_divisors

--- a/src/HOL/Divides.thy	Tue May 04 08:55:34 2010 +0200
+++ b/src/HOL/Divides.thy	Tue May 04 08:55:39 2010 +0200
@@ -379,6 +379,8 @@
 class ring_div = semiring_div + comm_ring_1
 begin
 
+subclass ring_1_no_zero_divisors ..
+
 text {* Negation respects modular equivalence. *}
 
 lemma mod_minus_eq: "(- a) mod b = (- (a mod b)) mod b"