diff -r 54b753b90b87 -r 38c01d7e9f5b src/HOL/Complex.thy --- 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 \ Re x = Re y \ Im x = Im y" by (auto intro: complex.expand) - - subsection \Addition and Subtraction\ instantiation complex :: ab_group_add