src/HOL/Complex.thy

--- a/src/HOL/Complex.thy	Thu Apr 09 20:42:38 2015 +0200
+++ b/src/HOL/Complex.thy	Sat Apr 11 11:56:40 2015 +0100
@@ -167,6 +167,10 @@
 lemma Im_divide_numeral [simp]: "Im (z / numeral w) = Im z / numeral w"
   by (simp add: Im_divide sqr_conv_mult)
 
+lemma of_real_Re [simp]:
+    "z \<in> \<real> \<Longrightarrow> of_real (Re z) = z"
+  by (auto simp: Reals_def)
+
 subsection {* The Complex Number $i$ *}
 
 primcorec "ii" :: complex  ("\<i>") where