# HG changeset patch
# User huffman
# Date 1158454416 -7200
# Node ID 759c8f2ead69aca3d75745e1a20575bcb1189260
# Parent  81dd3679f92c2b3cd395563f9c8844bae1fb7890
hcmod abbreviates hnorm :: hcomplex => hypreal

diff -r 81dd3679f92c -r 759c8f2ead69 src/HOL/Complex/NSComplex.thy
--- 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*}