# HG changeset patch
# User huffman
# Date 1315195434 25200
# Node ID 1a17d8913976f9755d17e8912c6b919bdbb0e137
# Parent  a8990b5d736535a5ca9f19fe66a7699f3cb56f05
tuned comments

diff -r a8990b5d7365 -r 1a17d8913976 src/HOL/Complex.thy
--- 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)