src/HOL/Divides.thy
changeset 20640 05e6042394b9
parent 20589 24ecf9bc1a0a
child 21191 c00161fbf990
     1.1 --- a/src/HOL/Divides.thy	Wed Sep 20 12:23:54 2006 +0200
     1.2 +++ b/src/HOL/Divides.thy	Wed Sep 20 12:24:11 2006 +0200
     1.3 @@ -896,6 +896,11 @@
     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 +
    1.12  hide (open) const divmod
    1.13  
    1.14