--- a/src/HOL/Complex_Analysis/Great_Picard.thy Mon Dec 02 22:40:16 2019 -0500
+++ b/src/HOL/Complex_Analysis/Great_Picard.thy Mon Dec 02 17:51:54 2019 +0100
@@ -4,7 +4,6 @@
theory Great_Picard
imports Conformal_Mappings
-
begin
subsection\<open>Schottky's theorem\<close>