# HG changeset patch
# User haftmann
# Date 1224863315 -7200
# Node ID 59c01ec6cb8d9d75040e8d52a5dbac1154d6c175
# Parent  5de9fc98ad961b6c9be280580a7dd724f73de890
more clever module name aliasses for code generation

diff -r 5de9fc98ad96 -r 59c01ec6cb8d src/HOL/Library/Efficient_Nat.thy
--- a/src/HOL/Library/Efficient_Nat.thy	Fri Oct 24 17:48:34 2008 +0200
+++ b/src/HOL/Library/Efficient_Nat.thy	Fri Oct 24 17:48:35 2008 +0200
@@ -445,16 +445,19 @@
 code_modulename SML
   Nat Integer
   Divides Integer
+  Ring_and_Field Integer
   Efficient_Nat Integer
 
 code_modulename OCaml
   Nat Integer
   Divides Integer
+  Ring_and_Field Integer
   Efficient_Nat Integer
 
 code_modulename Haskell
   Nat Integer
   Divides Integer
+  Ring_and_Field Integer
   Efficient_Nat Integer
 
 hide const int