src/HOL/Complex.thy

--- a/src/HOL/Complex.thy	Mon Mar 31 12:16:39 2014 +0200
+++ b/src/HOL/Complex.thy	Mon Mar 31 12:32:15 2014 +0200
@@ -232,6 +232,8 @@
 abbreviation complex_of_real :: "real \<Rightarrow> complex"
   where "complex_of_real \<equiv> of_real"
 
+declare [[coercion complex_of_real]]
+
 lemma complex_of_real_def: "complex_of_real r = Complex r 0"
   by (simp add: of_real_def complex_scaleR_def)