src/HOL/Divides.thy
changeset 22473 753123c89d72
parent 22261 9e185f78e7d4
child 22718 936f7580937d
     1.1 --- a/src/HOL/Divides.thy	Mon Mar 19 19:28:27 2007 +0100
     1.2 +++ b/src/HOL/Divides.thy	Tue Mar 20 08:27:15 2007 +0100
     1.3 @@ -12,7 +12,7 @@
     1.4  
     1.5  (*We use the same class for div and mod;
     1.6    moreover, dvd is defined whenever multiplication is*)
     1.7 -class div =
     1.8 +class div = type +
     1.9    fixes div :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
    1.10    fixes mod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
    1.11  begin