add complex_of_real coercion
authorhoelzl
Mon, 31 Mar 2014 12:32:15 +0200
changeset 56331 bea2196627cb
parent 56330 5c4d3be7a6b0
child 56332 289dd9166d04
add complex_of_real coercion
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)