--- a/src/HOL/Complex.thy Sun Sep 04 11:16:47 2011 -0700
+++ b/src/HOL/Complex.thy Sun Sep 04 21:03:54 2011 -0700
@@ -592,15 +592,14 @@
subsection{*Finally! Polar Form for Complex Numbers*}
-definition
+text {* An abbreviation for @{text "cos a + i sin a"}. *}
- (* abbreviation for (cos a + i sin a) *)
- cis :: "real => complex" where
+definition cis :: "real \<Rightarrow> complex" where
"cis a = Complex (cos a) (sin a)"
-definition
- (* abbreviation for r*(cos a + i sin a) *)
- rcis :: "[real, real] => complex" where
+text {* An abbreviation for @{text "r(cos a + i sin a)"}. *}
+
+definition rcis :: "[real, real] \<Rightarrow> complex" where
"rcis r a = complex_of_real r * cis a"
abbreviation expi :: "complex \<Rightarrow> complex"
@@ -660,11 +659,6 @@
lemma complex_In_mult_cnj_zero [simp]: "Im (z * cnj z) = 0"
by simp
-
-(*---------------------------------------------------------------------------*)
-(* (r1 * cis a) * (r2 * cis b) = r1 * r2 * cis (a + b) *)
-(*---------------------------------------------------------------------------*)
-
lemma cis_rcis_eq: "cis a = rcis 1 a"
by (simp add: rcis_def)