--- a/src/HOL/Library/Executable_Real.thy Sat May 19 11:33:20 2007 +0200
+++ b/src/HOL/Library/Executable_Real.thy Sat May 19 11:33:21 2007 +0200
@@ -467,6 +467,18 @@
"number_of k = real_int (number_of k)"
by (simp add: real_int_def)
+code_modulename SML
+ RealDef Real
+ Executable_Real Real
+
+code_modulename OCaml
+ RealDef Real
+ Executable_Real Real
+
+code_modulename Haskell
+ RealDef Real
+ Executable_Real Real
+
types_code real ("{* int * int *}")
attach (term_of) {*
fun term_of_real (p, q) =