# HG changeset patch
# User hoelzl
# Date 1396261935 -7200
# Node ID bea2196627cb7babeb060eb1200fe0ccde7dea4a
# Parent  5c4d3be7a6b023311cfc607b4e228cdd1d27afec
add complex_of_real coercion

diff -r 5c4d3be7a6b0 -r bea2196627cb 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)