src/HOL/Complex/NSCA.thy

--- a/src/HOL/Complex/NSCA.thy	Tue Jul 01 21:30:12 2008 +0200
+++ b/src/HOL/Complex/NSCA.thy	Wed Jul 02 07:11:57 2008 +0200
@@ -14,10 +14,9 @@
    SComplex  :: "hcomplex set" where
    "SComplex \<equiv> Standard"
 
-definition
-   stc :: "hcomplex => hcomplex" where
-    --{* standard part map*}
-   "stc x = (SOME r. x \<in> HFinite & r:SComplex & r @= x)"
+definition --{* standard part map*}
+  stc :: "hcomplex => hcomplex" where 
+  [code func del]: "stc x = (SOME r. x \<in> HFinite & r:SComplex & r @= x)"
 
 
 subsection{*Closure Laws for SComplex, the Standard Complex Numbers*}