--- a/src/HOL/Divides.thy Wed May 24 18:48:03 2000 +0200
+++ b/src/HOL/Divides.thy Wed May 24 18:48:22 2000 +0200
@@ -13,8 +13,8 @@
axclass
div < term
-instance
- nat :: div
+instance nat :: div
+instance nat :: plus_ac0 (add_commute,add_assoc,add_0)
consts
div :: ['a::div, 'a] => 'a (infixl 70)