# HG changeset patch
# User haftmann
# Date 1272956139 -7200
# Node ID f9b43d197d16b2255116693fcef13ee4e08ae551
# Parent  e4b15114869a050fbc883dd81a5151b424340011
a ring_div is a ring_1_no_zero_divisors

diff -r e4b15114869a -r f9b43d197d16 src/HOL/Divides.thy
--- 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"