
diff -r 8798edfc61ef -r 527088d4a89b src/HOL/Complex.thy
--- a/src/HOL/Complex.thy	Tue Aug 31 13:54:31 2021 +0200
+++ b/src/HOL/Complex.thy	Fri Sep 03 18:20:13 2021 +0100
@@ -27,6 +27,7 @@
   by (auto intro: complex.expand)
 
 
+
 subsection \<open>Addition and Subtraction\<close>
 
 instantiation complex :: ab_group_add
@@ -655,6 +656,9 @@
 
 subsection \<open>Basic Lemmas\<close>
 
+lemma complex_of_real_code[code_unfold]: "of_real = (\<lambda>x. Complex x 0)" 
+  by (intro ext, auto simp: complex_eq_iff)
+
 lemma complex_eq_0: "z=0 \<longleftrightarrow> (Re z)\<^sup>2 + (Im z)\<^sup>2 = 0"
   by (metis zero_complex.sel complex_eqI sum_power2_eq_zero_iff)
 




