src/HOL/Complex.thy
changeset 56331 bea2196627cb
parent 56238 5d147e1e18d1
child 56369 2704ca85be98
     1.1 --- a/src/HOL/Complex.thy	Mon Mar 31 12:16:39 2014 +0200
     1.2 +++ b/src/HOL/Complex.thy	Mon Mar 31 12:32:15 2014 +0200
     1.3 @@ -232,6 +232,8 @@
     1.4  abbreviation complex_of_real :: "real \<Rightarrow> complex"
     1.5    where "complex_of_real \<equiv> of_real"
     1.6  
     1.7 +declare [[coercion complex_of_real]]
     1.8 +
     1.9  lemma complex_of_real_def: "complex_of_real r = Complex r 0"
    1.10    by (simp add: of_real_def complex_scaleR_def)
    1.11