# HG changeset patch
# User huffman
# Date 1315340206 25200
# Node ID 0694fc3248fdec2aabaa18589d3b8f0aff1716aa
# Parent  19e1c6e922b60473a5703ccc20595f13b6c45cc2
remove some unnecessary simp rules from simpset

diff -r 19e1c6e922b6 -r 0694fc3248fd src/HOL/Complex.thy
--- 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)