src/HOL/Complex.thy
changeset 59000 6eb0725503fc
parent 58889 5b7a9633cfa8
child 59613 7103019278f0
--- a/src/HOL/Complex.thy	Thu Nov 13 14:40:06 2014 +0100
+++ b/src/HOL/Complex.thy	Thu Nov 13 17:19:52 2014 +0100
@@ -132,7 +132,8 @@
 abbreviation complex_of_real :: "real \<Rightarrow> complex"
   where "complex_of_real \<equiv> of_real"
 
-declare [[coercion complex_of_real]]
+declare [[coercion "of_real :: real \<Rightarrow> complex"]]
+declare [[coercion "of_rat :: rat \<Rightarrow> complex"]]
 declare [[coercion "of_int :: int \<Rightarrow> complex"]]
 declare [[coercion "of_nat :: nat \<Rightarrow> complex"]]