# HG changeset patch
# User wenzelm
# Date 1205789665 -3600
# Node ID 81a0fc28b0de5d0ac645ad09a54a65cad16ef3b6
# Parent  f8a7fac36e13ca05293d37b5dbe721eb16935488
removed duplicate lemmas;

diff -r f8a7fac36e13 -r 81a0fc28b0de src/HOL/Complex/Complex.thy
--- a/src/HOL/Complex/Complex.thy	Mon Mar 17 22:34:23 2008 +0100
+++ b/src/HOL/Complex/Complex.thy	Mon Mar 17 22:34:25 2008 +0100
@@ -624,12 +624,6 @@
 lemma complex_mod_rcis [simp]: "cmod(rcis r a) = abs r"
 by (simp add: rcis_def cis_def sin_cos_squared_add2_mult)
 
-lemma complex_Re_cnj [simp]: "Re(cnj z) = Re z"
-by (induct z, simp add: complex_cnj)
-
-lemma complex_Im_cnj [simp]: "Im(cnj z) = - Im z"
-by (induct z, simp add: complex_cnj)
-
 lemma complex_mod_sqrt_Re_mult_cnj: "cmod z = sqrt (Re (z * cnj z))"
 by (simp add: cmod_def power2_eq_square)