# HG changeset patch
# User nipkow
# Date 1572958582 -3600
# Node ID 66c02538342235fd66fb71d45c564eeaba36725c
# Parent  c2465b429e6e06f60fa36bf319a7a0a34419eb51
tuned

diff -r c2465b429e6e -r 66c025383422 src/HOL/Analysis/Cauchy_Integral_Theorem.thy
--- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Mon Nov 04 19:53:43 2019 -0500
+++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Tue Nov 05 13:56:22 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>)"
diff -r c2465b429e6e -r 66c025383422 src/HOL/Analysis/Lindelof_Spaces.thy
--- a/src/HOL/Analysis/Lindelof_Spaces.thy	Mon Nov 04 19:53:43 2019 -0500
+++ b/src/HOL/Analysis/Lindelof_Spaces.thy	Tue Nov 05 13:56:22 2019 +0100
@@ -1,4 +1,4 @@
-section\<open>Lindelof spaces\<close>
+section\<open>Lindel\"of spaces\<close>
 
 theory Lindelof_Spaces
 imports T1_Spaces
diff -r c2465b429e6e -r 66c025383422 src/HOL/Analysis/Retracts.thy
--- a/src/HOL/Analysis/Retracts.thy	Mon Nov 04 19:53:43 2019 -0500
+++ b/src/HOL/Analysis/Retracts.thy	Tue Nov 05 13:56:22 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.
diff -r c2465b429e6e -r 66c025383422 src/HOL/Analysis/Winding_Numbers.thy
--- a/src/HOL/Analysis/Winding_Numbers.thy	Mon Nov 04 19:53:43 2019 -0500
+++ b/src/HOL/Analysis/Winding_Numbers.thy	Tue Nov 05 13:56:22 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: