--- a/src/HOL/Complex_Main.thy Sun May 12 23:23:39 2024 +0100 +++ b/src/HOL/Complex_Main.thy Mon May 13 22:42:40 2024 +0100 @@ -4,6 +4,7 @@ imports Complex MacLaurin + Binomial_Plus begin end \ No newline at end of file