src/HOL/Divides.thy

--- a/src/HOL/Divides.thy	Tue Jan 17 10:26:50 2006 +0100
+++ b/src/HOL/Divides.thy	Tue Jan 17 16:36:57 2006 +0100
@@ -870,6 +870,13 @@
 apply (rule mod_add1_eq [symmetric])
 done
 
+subsection {* Code generator setup *}
+
+code_alias
+  "Divides.op div" "Divides.div"
+  "Divides.op dvd" "Divides.dvd"
+  "Divides.op mod" "Divides.mod"
+
 ML
 {*
 val div_def = thm "div_def"