src/HOL/Divides.thy
changeset 23948 261bd4678076
parent 23684 8c508c4dc53b
child 24268 9b4d7c59cc90
     1.1 --- a/src/HOL/Divides.thy	Mon Jul 23 22:18:05 2007 +0200
     1.2 +++ b/src/HOL/Divides.thy	Tue Jul 24 15:20:45 2007 +0200
     1.3 @@ -26,12 +26,10 @@
     1.4  definition (in times)
     1.5    dvd  :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl "\<^loc>dvd" 50)
     1.6  where
     1.7 -  "m \<^loc>dvd n \<longleftrightarrow> (\<exists>k. n = m \<^loc>* k)"
     1.8 -lemmas dvd_def = dvd_def [folded times_class.dvd]
     1.9 +  [code func del]: "m \<^loc>dvd n \<longleftrightarrow> (\<exists>k. n = m \<^loc>* k)"
    1.10  
    1.11  class dvd_mod = times + div + zero + -- {* for code generation *}
    1.12 -  assumes dvd_def_mod: "times.dvd (op \<^loc>*) x y \<longleftrightarrow> y \<^loc>mod x = \<^loc>0"
    1.13 -lemmas dvd_def_mod [code func] = dvd_def_mod [folded times_class.dvd]
    1.14 +  assumes dvd_def_mod [code func]: "times.dvd (op \<^loc>*) x y \<longleftrightarrow> y \<^loc>mod x = \<^loc>0"
    1.15  
    1.16  definition
    1.17    quorem :: "(nat*nat) * (nat*nat) => bool" where