# HG changeset patch
# User paulson
# Date 959186902 -7200
# Node ID b547482dd127f96cf9306bdda8f39413ed2ca0a1
# Parent  0cd01ec1830b0cf3bae933fecd74cad918cd1e2e
installing plus_ac0 for nat

diff -r 0cd01ec1830b -r b547482dd127 src/HOL/Divides.thy
--- 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)