# HG changeset patch
# User nipkow
# Date 1179574833 -7200
# Node ID c7ff1537c4bf86073319e127803bda78dafc9f0d
# Parent  79ee75dc1e593e405a26fde03a348faaa4b9eb96
Disabled Stefancs code generator - already enabled in RealDef.

diff -r 79ee75dc1e59 -r c7ff1537c4bf src/HOL/Library/Executable_Real.thy
--- a/src/HOL/Library/Executable_Real.thy	Sat May 19 11:33:57 2007 +0200
+++ b/src/HOL/Library/Executable_Real.thy	Sat May 19 13:40:33 2007 +0200
@@ -479,6 +479,7 @@
   RealDef Real
   Executable_Real Real
 
+(* There is already an implementation in RealDef
 types_code real ("{* int * int *}")
 attach (term_of) {*
 fun term_of_real (p, q) =
@@ -492,5 +493,5 @@
 *}
 
 consts_code INum ("")
-
-end
\ No newline at end of file
+*)
+end