# HG changeset patch
# User haftmann
# Date 1218486345 -7200
# Node ID 29151fa7c58e657d0513f437f4bf927df67fb1ef
# Parent  992c6d9849254af3709190a4d1e0054062e36585
rudimentary code setup for set operations

diff -r 992c6d984925 -r 29151fa7c58e src/HOL/Real/RealDef.thy
--- a/src/HOL/Real/RealDef.thy	Mon Aug 11 22:06:51 2008 +0200
+++ b/src/HOL/Real/RealDef.thy	Mon Aug 11 22:25:45 2008 +0200
@@ -23,7 +23,7 @@
 definition
   (** these don't use the overloaded "real" function: users don't see them **)
   real_of_preal :: "preal => real" where
-  "real_of_preal m = Abs_Real(realrel``{(m + 1, 1)})"
+  [code func del]: "real_of_preal m = Abs_Real (realrel `` {(m + 1, 1)})"
 
 instantiation real :: "{zero, one, plus, minus, uminus, times, inverse, ord, abs, sgn}"
 begin