src/HOL/NSA/NSComplex.thy
changeset 60017 b785d6d06430
parent 59730 b7c394c7a619
child 60867 86e7560e07d0
     1.1 --- a/src/HOL/NSA/NSComplex.thy	Thu Apr 09 20:42:38 2015 +0200
     1.2 +++ b/src/HOL/NSA/NSComplex.thy	Sat Apr 11 11:56:40 2015 +0100
     1.3 @@ -72,7 +72,7 @@
     1.4    (*------------ e ^ (x + iy) ------------*)
     1.5  definition
     1.6    hExp :: "hcomplex => hcomplex" where
     1.7 -  "hExp = *f* Exp"
     1.8 +  "hExp = *f* exp"
     1.9  
    1.10  definition
    1.11    HComplex :: "[hypreal,hypreal] => hcomplex" where
    1.12 @@ -485,7 +485,7 @@
    1.13  by transfer (rule rcis_Ex)
    1.14  
    1.15  lemma hRe_hcomplex_polar [simp]:
    1.16 -  "!!r a. hRe (hcomplex_of_hypreal r * HComplex (( *f* cos) a) (( *f* sin) a)) = 
    1.17 +  "!!r a. hRe (hcomplex_of_hypreal r * HComplex (( *f* cos) a) (( *f* sin) a)) =
    1.18        r * ( *f* cos) a"
    1.19  by transfer simp
    1.20  
    1.21 @@ -493,7 +493,7 @@
    1.22  by transfer (rule Re_rcis)
    1.23  
    1.24  lemma hIm_hcomplex_polar [simp]:
    1.25 -  "!!r a. hIm (hcomplex_of_hypreal r * HComplex (( *f* cos) a) (( *f* sin) a)) = 
    1.26 +  "!!r a. hIm (hcomplex_of_hypreal r * HComplex (( *f* cos) a) (( *f* sin) a)) =
    1.27        r * ( *f* sin) a"
    1.28  by transfer simp
    1.29  
    1.30 @@ -621,8 +621,8 @@
    1.31  
    1.32  subsection{*Numerals and Arithmetic*}
    1.33  
    1.34 -lemma hcomplex_of_hypreal_eq_hcomplex_of_complex: 
    1.35 -     "hcomplex_of_hypreal (hypreal_of_real x) =  
    1.36 +lemma hcomplex_of_hypreal_eq_hcomplex_of_complex:
    1.37 +     "hcomplex_of_hypreal (hypreal_of_real x) =
    1.38        hcomplex_of_complex (complex_of_real x)"
    1.39  by transfer (rule refl)
    1.40  
    1.41 @@ -642,15 +642,15 @@
    1.42        "hcmod(numeral v :: hcomplex) = (numeral v :: hypreal)"
    1.43  by transfer (rule norm_numeral)
    1.44  
    1.45 -lemma hcomplex_neg_numeral_hcmod [simp]: 
    1.46 +lemma hcomplex_neg_numeral_hcmod [simp]:
    1.47        "hcmod(- numeral v :: hcomplex) = (numeral v :: hypreal)"
    1.48  by transfer (rule norm_neg_numeral)
    1.49  
    1.50 -lemma hcomplex_numeral_hRe [simp]: 
    1.51 +lemma hcomplex_numeral_hRe [simp]:
    1.52        "hRe(numeral v :: hcomplex) = numeral v"
    1.53  by transfer (rule complex_Re_numeral)
    1.54  
    1.55 -lemma hcomplex_numeral_hIm [simp]: 
    1.56 +lemma hcomplex_numeral_hIm [simp]:
    1.57        "hIm(numeral v :: hcomplex) = 0"
    1.58  by transfer (rule complex_Im_numeral)
    1.59