--- a/src/HOL/Complex/NSComplex.thy Sat Sep 16 23:46:38 2006 +0200
+++ b/src/HOL/Complex/NSComplex.thy Sun Sep 17 02:53:36 2006 +0200
@@ -17,6 +17,9 @@
hcomplex_of_complex :: "complex => complex star"
"hcomplex_of_complex == star_of"
+ hcmod :: "complex star => real star"
+ "hcmod == hnorm"
+
definition
(*--- real and Imaginary parts ---*)
@@ -28,11 +31,6 @@
"hIm = *f* Im"
- (*----------- modulus ------------*)
-
- hcmod :: "hcomplex => hypreal"
- "hcmod = *f* cmod"
-
(*------ imaginary unit ----------*)
iii :: hcomplex
@@ -76,9 +74,12 @@
"(z::hcomplex) hcpow (n::hypnat) = ( *f2* op ^) z n"
lemmas hcomplex_defs [transfer_unfold] =
- hRe_def hIm_def hcmod_def iii_def hcnj_def hsgn_def harg_def hcis_def
+ hRe_def hIm_def iii_def hcnj_def hsgn_def harg_def hcis_def
hcomplex_of_hypreal_def hrcis_def hexpi_def HComplex_def hcpow_def
+lemma hcmod_def: "hcmod = *f* cmod"
+by (rule hnorm_def)
+
subsection{*Properties of Nonstandard Real and Imaginary Parts*}