--- a/src/HOL/Complex/NSCA.thy Fri Nov 17 02:19:55 2006 +0100
+++ b/src/HOL/Complex/NSCA.thy Fri Nov 17 02:20:03 2006 +0100
@@ -11,10 +11,11 @@
definition
(* standard complex numbers reagarded as an embedded subset of NS complex *)
- SComplex :: "hcomplex set"
+ SComplex :: "hcomplex set" where
"SComplex = {x. \<exists>r. x = hcomplex_of_complex r}"
- stc :: "hcomplex => hcomplex"
+definition
+ stc :: "hcomplex => hcomplex" where
--{* standard part map*}
"stc x = (SOME r. x \<in> HFinite & r:SComplex & r @= x)"