diff -r fc571ebb04e1 -r 6eb0725503fc src/HOL/Complex.thy --- 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 \ complex" where "complex_of_real \ of_real" -declare [[coercion complex_of_real]] +declare [[coercion "of_real :: real \ complex"]] +declare [[coercion "of_rat :: rat \ complex"]] declare [[coercion "of_int :: int \ complex"]] declare [[coercion "of_nat :: nat \ complex"]]