--- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy Tue Nov 05 12:00:23 2019 +0000
+++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy Tue Nov 05 13:56:34 2019 +0100
@@ -3,7 +3,11 @@
text\<open>By John Harrison et al. Ported from HOL Light by L C Paulson (2015)\<close>
theory Cauchy_Integral_Theorem
-imports Complex_Transcendental Henstock_Kurzweil_Integration Weierstrass_Theorems Retracts
+imports
+ Complex_Transcendental
+ Henstock_Kurzweil_Integration
+ Weierstrass_Theorems
+ Retracts
begin
lemma leibniz_rule_holomorphic:
@@ -4306,7 +4310,7 @@
by (auto simp: open_dist)
qed
-subsection\<open>Winding number is zero "outside" a curve, in various senses\<close>
+subsection\<open>Winding number is zero "outside" a curve\<close>
proposition winding_number_zero_in_outside:
assumes \<gamma>: "path \<gamma>" and loop: "pathfinish \<gamma> = pathstart \<gamma>" and z: "z \<in> outside (path_image \<gamma>)"
--- a/src/HOL/Analysis/Lindelof_Spaces.thy Tue Nov 05 12:00:23 2019 +0000
+++ b/src/HOL/Analysis/Lindelof_Spaces.thy Tue Nov 05 13:56:34 2019 +0100
@@ -1,4 +1,4 @@
-section\<open>Lindelof spaces\<close>
+section\<open>Lindel\"of spaces\<close>
theory Lindelof_Spaces
imports T1_Spaces
--- a/src/HOL/Analysis/Retracts.thy Tue Nov 05 12:00:23 2019 +0000
+++ b/src/HOL/Analysis/Retracts.thy Tue Nov 05 13:56:34 2019 +0100
@@ -1,10 +1,12 @@
section \<open>Absolute Retracts, Absolute Neighbourhood Retracts and Euclidean Neighbourhood Retracts\<close>
theory Retracts
- imports Brouwer_Fixpoint Continuous_Extension Ordered_Euclidean_Space
+imports
+ Brouwer_Fixpoint
+ Continuous_Extension
+ Ordered_Euclidean_Space
begin
-
text \<open>Absolute retracts (AR), absolute neighbourhood retracts (ANR) and also Euclidean neighbourhood
retracts (ENR). We define AR and ANR by specializing the standard definitions for a set to embedding
in spaces of higher dimension.
--- a/src/HOL/Analysis/Winding_Numbers.thy Tue Nov 05 12:00:23 2019 +0000
+++ b/src/HOL/Analysis/Winding_Numbers.thy Tue Nov 05 13:56:34 2019 +0100
@@ -3,7 +3,10 @@
text\<open>By John Harrison et al. Ported from HOL Light by L C Paulson (2017)\<close>
theory Winding_Numbers
-imports Polytope Jordan_Curve Riemann_Mapping
+imports
+ Polytope
+ Jordan_Curve
+ Riemann_Mapping
begin
lemma simply_connected_inside_simple_path: