1.1 --- a/src/HOL/Divides.thy	Tue Jan 17 10:26:50 2006 +0100
     1.2 +++ b/src/HOL/Divides.thy	Tue Jan 17 16:36:57 2006 +0100
     1.3 @@ -870,6 +870,13 @@
     1.4  apply (rule mod_add1_eq [symmetric])
     1.5  done
     1.6  
     1.7 +subsection {* Code generator setup *}
     1.8 +
     1.9 +code_alias
    1.10 +  "Divides.op div" "Divides.div"
    1.11 +  "Divides.op dvd" "Divides.dvd"
    1.12 +  "Divides.op mod" "Divides.mod"
    1.13 +
    1.14  ML
    1.15  {*
    1.16  val div_def = thm "div_def"