src/HOL/Complex.thy
changeset 74226 38c01d7e9f5b
parent 74223 527088d4a89b
child 75494 eded3fe9e600
--- a/src/HOL/Complex.thy	Fri Sep 03 22:53:11 2021 +0100
+++ b/src/HOL/Complex.thy	Sat Sep 04 11:22:24 2021 +0100
@@ -26,8 +26,6 @@
 lemma complex_eq_iff: "x = y \<longleftrightarrow> Re x = Re y \<and> Im x = Im y"
   by (auto intro: complex.expand)
 
-
-
 subsection \<open>Addition and Subtraction\<close>
 
 instantiation complex :: ab_group_add