# HG changeset patch
# User haftmann
# Date 1184081452 -7200
# Node ID dc452e8641aac3e6b59b20f381bd3abd0c0fb3ad
# Parent  a8ac2305eaf23db68bfe5f607741086404ebe91c
improvement for code names

diff -r a8ac2305eaf2 -r dc452e8641aa src/HOL/Library/EfficientNat.thy
--- a/src/HOL/Library/EfficientNat.thy	Tue Jul 10 17:30:51 2007 +0200
+++ b/src/HOL/Library/EfficientNat.thy	Tue Jul 10 17:30:52 2007 +0200
@@ -385,14 +385,17 @@
 *}
 (*>*)
 
+
 subsection {* Module names *}
 
 code_modulename SML
   Nat Integer
+  Divides Integer
   EfficientNat Integer
 
 code_modulename OCaml
   Nat Integer
+  Divides Integer
   EfficientNat Integer
 
 code_modulename Haskell