--- a/src/HOL/Analysis/Conformal_Mappings.thy Tue Jan 16 09:12:16 2018 +0100
+++ b/src/HOL/Analysis/Conformal_Mappings.thy Tue Jan 16 09:30:00 2018 +0100
@@ -980,7 +980,7 @@
proof -
have f0: "(f \<longlongrightarrow> 0) at_infinity"
proof -
- have DIM_complex[intro]: "2 \<le> DIM(complex)" \<comment>\<open>should not be necessary!\<close>
+ have DIM_complex[intro]: "2 \<le> DIM(complex)" \<comment> \<open>should not be necessary!\<close>
by simp
have "continuous_on (inverse ` (ball 0 r - {0})) f"
using continuous_on_subset holf holomorphic_on_imp_continuous_on by blast