# HG changeset patch
# User huffman
# Date 1181140959 -7200
# Node ID 339cdc29b0bc3ca61e6f047742eee35ecfb63d3c
# Parent  f997514ad8f40fb6f690b1d6cb43e167cc8bb906
declare complex_diff as simp rule

diff -r f997514ad8f4 -r 339cdc29b0bc src/HOL/Complex/Complex.thy
--- a/src/HOL/Complex/Complex.thy	Wed Jun 06 16:12:08 2007 +0200
+++ b/src/HOL/Complex/Complex.thy	Wed Jun 06 16:42:39 2007 +0200
@@ -75,7 +75,7 @@
 lemma complex_Im_minus [simp]: "Im (- x) = - Im x"
 by (simp add: complex_minus_def)
 
-lemma complex_diff:
+lemma complex_diff [simp]:
   "Complex a b - Complex c d = Complex (a - c) (b - d)"
 by (simp add: complex_diff_def)
 
@@ -363,7 +363,6 @@
 apply (drule_tac r="r / sqrt 2" in LIMSEQ_D, safe)
 apply (drule_tac r="r / sqrt 2" in LIMSEQ_D, safe)
 apply (rename_tac M N, rule_tac x="max M N" in exI, safe)
-apply (simp add: complex_diff)
 apply (simp add: real_sqrt_sum_squares_less)
 apply (simp add: divide_pos_pos)
 done