src/HOL/Divides.thy
changeset 24748 ee0a0eb6b738
parent 24286 7619080e49f0
child 24993 92dfacb32053
     1.1 --- a/src/HOL/Divides.thy	Fri Sep 28 10:35:53 2007 +0200
     1.2 +++ b/src/HOL/Divides.thy	Sat Sep 29 08:58:51 2007 +0200
     1.3 @@ -29,7 +29,7 @@
     1.4    [code func del]: "m \<^loc>dvd n \<longleftrightarrow> (\<exists>k. n = m \<^loc>* k)"
     1.5  
     1.6  class dvd_mod = times + div + zero + -- {* for code generation *}
     1.7 -  assumes dvd_def_mod [code func]: "times.dvd (op \<^loc>*) x y \<longleftrightarrow> y \<^loc>mod x = \<^loc>0"
     1.8 +  assumes dvd_def_mod [code func]: "x \<^loc>dvd y \<longleftrightarrow> y \<^loc>mod x = \<^loc>0"
     1.9  
    1.10  definition
    1.11    quorem :: "(nat*nat) * (nat*nat) => bool" where
    1.12 @@ -880,8 +880,6 @@
    1.13  qed
    1.14  
    1.15  
    1.16 -
    1.17 -
    1.18  subsection {* Code generation for div, mod and dvd on nat *}
    1.19  
    1.20  definition [code func del]: