--- a/src/HOL/Complex.thy Tue Sep 06 21:56:11 2011 +0200
+++ b/src/HOL/Complex.thy Tue Sep 06 13:16:46 2011 -0700
@@ -304,10 +304,10 @@
end
-lemma cmod_unit_one [simp]: "cmod (Complex (cos a) (sin a)) = 1"
+lemma cmod_unit_one: "cmod (Complex (cos a) (sin a)) = 1"
by simp
-lemma cmod_complex_polar [simp]:
+lemma cmod_complex_polar:
"cmod (complex_of_real r * Complex (cos a) (sin a)) = abs r"
by (simp add: norm_mult)
@@ -315,10 +315,10 @@
unfolding complex_norm_def
by (rule real_sqrt_sum_squares_ge1)
-lemma complex_mod_minus_le_complex_mod [simp]: "- cmod x \<le> cmod x"
+lemma complex_mod_minus_le_complex_mod: "- cmod x \<le> cmod x"
by (rule order_trans [OF _ norm_ge_zero], simp)
-lemma complex_mod_triangle_ineq2 [simp]: "cmod(b + a) - cmod b \<le> cmod a"
+lemma complex_mod_triangle_ineq2: "cmod(b + a) - cmod b \<le> cmod a"
by (rule ord_le_eq_trans [OF norm_triangle_ineq2], simp)
lemma abs_Re_le_cmod: "\<bar>Re x\<bar> \<le> cmod x"
@@ -635,7 +635,7 @@
qed
lemma complex_mod_rcis [simp]: "cmod(rcis r a) = abs r"
- by (simp add: rcis_def cis_def sin_cos_squared_add2_mult)
+ by (simp add: rcis_def cis_def norm_mult)
lemma complex_mod_sqrt_Re_mult_cnj: "cmod z = sqrt (Re (z * cnj z))"
by (simp add: cmod_def power2_eq_square)