src/HOL/Divides.thy
changeset 8902 a705822f4e2a
parent 7029 08d4eb8500dd
child 8961 b547482dd127
--- a/src/HOL/Divides.thy	Sun May 21 14:44:01 2000 +0200
+++ b/src/HOL/Divides.thy	Sun May 21 14:49:28 2000 +0200
@@ -8,13 +8,13 @@
 
 Divides = Arith +
 
-(*We use the same sort for div and mod;
+(*We use the same class for div and mod;
   moreover, dvd is defined whenever multiplication is*)
 axclass
   div < term
 
 instance
-  nat :: {div}
+  nat :: div
 
 consts
   div  :: ['a::div, 'a]  => 'a          (infixl 70)