src/HOL/Divides.thy
changeset 21191 c00161fbf990
parent 20640 05e6042394b9
child 21408 fff1731da03b
     1.1 --- a/src/HOL/Divides.thy	Mon Nov 06 16:28:30 2006 +0100
     1.2 +++ b/src/HOL/Divides.thy	Mon Nov 06 16:28:31 2006 +0100
     1.3 @@ -896,10 +896,8 @@
     1.4    "m mod n = snd (divmod m n)"
     1.5    unfolding divmod_def by simp
     1.6  
     1.7 -code_constname
     1.8 -  "op div \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat" "IntDef.div_nat"
     1.9 -  "op mod \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat" "IntDef.mod_nat"
    1.10 -  Divides.divmod "IntDef.divmod_nat"
    1.11 +code_modulename SML
    1.12 +  Divides Integer
    1.13  
    1.14  hide (open) const divmod
    1.15