author | paulson <lp15@cam.ac.uk> |
Sat, 04 Sep 2021 11:22:24 +0100 | |
changeset 74226 | 38c01d7e9f5b |
parent 74225 | 54b753b90b87 |
child 74250 | cbbd08df65bd |
--- 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