tuned comments
authorhuffman
Sun Sep 04 21:03:54 2011 -0700 (2011-09-04)
changeset 447151a17d8913976
parent 44714 a8990b5d7365
child 44716 d37afb90c23e
tuned comments
src/HOL/Complex.thy
     1.1 --- a/src/HOL/Complex.thy	Sun Sep 04 11:16:47 2011 -0700
     1.2 +++ b/src/HOL/Complex.thy	Sun Sep 04 21:03:54 2011 -0700
     1.3 @@ -592,15 +592,14 @@
     1.4  
     1.5  subsection{*Finally! Polar Form for Complex Numbers*}
     1.6  
     1.7 -definition
     1.8 +text {* An abbreviation for @{text "cos a + i sin a"}. *}
     1.9  
    1.10 -  (* abbreviation for (cos a + i sin a) *)
    1.11 -  cis :: "real => complex" where
    1.12 +definition cis :: "real \<Rightarrow> complex" where
    1.13    "cis a = Complex (cos a) (sin a)"
    1.14  
    1.15 -definition
    1.16 -  (* abbreviation for r*(cos a + i sin a) *)
    1.17 -  rcis :: "[real, real] => complex" where
    1.18 +text {* An abbreviation for @{text "r(cos a + i sin a)"}. *}
    1.19 +
    1.20 +definition rcis :: "[real, real] \<Rightarrow> complex" where
    1.21    "rcis r a = complex_of_real r * cis a"
    1.22  
    1.23  abbreviation expi :: "complex \<Rightarrow> complex"
    1.24 @@ -660,11 +659,6 @@
    1.25  lemma complex_In_mult_cnj_zero [simp]: "Im (z * cnj z) = 0"
    1.26  by simp
    1.27  
    1.28 -
    1.29 -(*---------------------------------------------------------------------------*)
    1.30 -(*  (r1 * cis a) * (r2 * cis b) = r1 * r2 * cis (a + b)                      *)
    1.31 -(*---------------------------------------------------------------------------*)
    1.32 -
    1.33  lemma cis_rcis_eq: "cis a = rcis 1 a"
    1.34  by (simp add: rcis_def)
    1.35