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)