src/HOL/Complex.thy
changeset 60017 b785d6d06430
parent 59867 58043346ca64
child 60352 d46de31a50c4
     1.1 --- a/src/HOL/Complex.thy	Thu Apr 09 20:42:38 2015 +0200
     1.2 +++ b/src/HOL/Complex.thy	Sat Apr 11 11:56:40 2015 +0100
     1.3 @@ -167,6 +167,10 @@
     1.4  lemma Im_divide_numeral [simp]: "Im (z / numeral w) = Im z / numeral w"
     1.5    by (simp add: Im_divide sqr_conv_mult)
     1.6  
     1.7 +lemma of_real_Re [simp]:
     1.8 +    "z \<in> \<real> \<Longrightarrow> of_real (Re z) = z"
     1.9 +  by (auto simp: Reals_def)
    1.10 +
    1.11  subsection {* The Complex Number $i$ *}
    1.12  
    1.13  primcorec "ii" :: complex  ("\<i>") where