# HG changeset patch
# User huffman
# Date 1180482818 -7200
# Node ID 93f8cb025afdd38068e56f3e61decc5819a87ede
# Parent  6f7b5b96241fa1834db5e9ffd10f9d62733b0531
renamed some lemmas in Complex.thy

diff -r 6f7b5b96241f -r 93f8cb025afd src/HOL/Complex/NSComplex.thy
--- a/src/HOL/Complex/NSComplex.thy	Wed May 30 01:46:05 2007 +0200
+++ b/src/HOL/Complex/NSComplex.thy	Wed May 30 01:53:38 2007 +0200
@@ -360,15 +360,15 @@
 lemma hcomplexpow_Suc [simp]: "z ^ (Suc n) = (z::hcomplex) * (z ^ n)"
 by (rule power_Suc)
 
-lemma hcomplexpow_i_squared [simp]: "iii ^ 2 = - 1"
-by transfer (rule complexpow_i_squared)
+lemma hcomplexpow_i_squared [simp]: "iii ^ 2 = -1"
+by transfer (rule power2_i)
 
 lemma hcomplex_of_hypreal_pow:
      "!!x. hcomplex_of_hypreal (x ^ n) = (hcomplex_of_hypreal x) ^ n"
 by transfer (rule of_real_power)
 
 lemma hcomplex_hcnj_pow: "!!z. hcnj(z ^ n) = hcnj(z) ^ n"
-by transfer (rule complex_cnj_pow)
+by transfer (rule complex_cnj_power)
 
 lemma hcmod_hcomplexpow: "!!x. hcmod(x ^ n) = hcmod(x) ^ n"
 by transfer (rule norm_power)
@@ -408,7 +408,7 @@
 by transfer (rule sgn_eq)
 
 lemma hcmod_i: "!!x y. hcmod (HComplex x y) = ( *f* sqrt) (x ^ 2 + y ^ 2)"
-by transfer (rule complex_mod)
+by transfer (rule complex_norm)
 
 lemma hcomplex_eq_cancel_iff1 [simp]:
      "(hcomplex_of_hypreal xa = HComplex x y) = (xa = x & y = 0)"
@@ -653,7 +653,7 @@
 
 lemma hcomplex_hypreal_number_of: 
   "hcomplex_of_complex (number_of w) = hcomplex_of_hypreal(number_of w)"
-by transfer (rule complex_number_of [symmetric])
+by transfer (rule of_real_number_of_eq [symmetric])
 
 (*
 Goal "z + hcnj z =  
@@ -759,18 +759,18 @@
 
 lemma hcomplex_number_of_hcnj [simp]:
      "hcnj (number_of v :: hcomplex) = number_of v"
-by transfer (rule complex_number_of_cnj)
+by transfer (rule complex_cnj_number_of)
 
 lemma hcomplex_number_of_hcmod [simp]: 
       "hcmod(number_of v :: hcomplex) = abs (number_of v :: hypreal)"
-by transfer (rule complex_number_of_cmod)
+by transfer (rule norm_number_of)
 
 lemma hcomplex_number_of_hRe [simp]: 
       "hRe(number_of v :: hcomplex) = number_of v"
-by transfer (rule complex_number_of_Re)
+by transfer (rule complex_Re_number_of)
 
 lemma hcomplex_number_of_hIm [simp]: 
       "hIm(number_of v :: hcomplex) = 0"
-by transfer (rule complex_number_of_Im)
+by transfer (rule complex_Im_number_of)
 
 end