--- a/src/HOL/Analysis/Jordan_Curve.thy Fri Apr 12 19:48:29 2019 +0200
+++ b/src/HOL/Analysis/Jordan_Curve.thy Fri Apr 12 22:09:25 2019 +0200
@@ -219,7 +219,7 @@
qed
-theorem%unimportant Jordan_curve:
+theorem\<^marker>\<open>tag unimportant\<close> 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%unimportant Jordan_disconnected:
+corollary\<^marker>\<open>tag unimportant\<close> Jordan_disconnected:
fixes c :: "real \<Rightarrow> complex"
assumes "simple_path c" "pathfinish c = pathstart c"
shows "\<not> connected(- path_image c)"