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