diff -r 7538b5f301ea -r 16d98ef49a2c src/HOL/Analysis/Jordan_Curve.thy
--- a/src/HOL/Analysis/Jordan_Curve.thy	Wed Jul 18 17:01:12 2018 +0200
+++ b/src/HOL/Analysis/Jordan_Curve.thy	Tue Jul 17 12:23:37 2018 +0200
@@ -6,7 +6,6 @@
 
 theory Jordan_Curve
   imports Arcwise_Connected Further_Topology
-
 begin
 
 subsection\<open>Janiszewski's theorem\<close>
@@ -114,8 +113,8 @@
 
 
 theorem Janiszewski:
-  fixes a b::complex
-  assumes "compact S" "closed T" and conST: "connected(S \<inter> T)"
+  fixes a b :: complex
+  assumes "compact S" "closed T" and conST: "connected (S \<inter> T)"
       and ccS: "connected_component (- S) a b" and ccT: "connected_component (- T) a b"
     shows "connected_component (- (S \<union> T)) a b"
 proof -
@@ -166,6 +165,7 @@
 using Janiszewski [OF ST]
 by (metis IntD1 IntD2 notST compl_sup connected_iff_connected_component)
 
+
 subsection\<open>The Jordan Curve theorem\<close>
 
 lemma exists_double_arc:
@@ -219,7 +219,7 @@
 qed
 
 
-theorem Jordan_curve:
+theorem%unimportant Jordan_curve:
   fixes c :: "real \<Rightarrow> complex"
   assumes "simple_path c" and loop: "pathfinish c = pathstart c"
   obtains inner outer where
@@ -389,7 +389,7 @@
 qed
 
 
-corollary Jordan_disconnected:
+corollary%unimportant Jordan_disconnected:
   fixes c :: "real \<Rightarrow> complex"
   assumes "simple_path c" "pathfinish c = pathstart c"
     shows "\<not> connected(- path_image c)"