add complex_of_real coercion
authorhoelzl
Mon Mar 31 12:32:15 2014 +0200 (2014-03-31)
changeset 56331bea2196627cb
parent 56330 5c4d3be7a6b0
child 56332 289dd9166d04
add complex_of_real coercion
src/HOL/Complex.thy
     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