src/HOL/Divides.thy
changeset 10214 77349ed89f45
parent 10212 33fe2d701ddd
child 10559 d3fd54fc659b
--- a/src/HOL/Divides.thy	Thu Oct 12 18:44:35 2000 +0200
+++ b/src/HOL/Divides.thy	Fri Oct 13 08:28:21 2000 +0200
@@ -6,7 +6,7 @@
 The division operators div, mod and the divides relation "dvd"
 *)
 
-Divides = Arithmetic +
+Divides = NatArith +
 
 (*We use the same class for div and mod;
   moreover, dvd is defined whenever multiplication is*)