--- a/src/HOL/Analysis/Continuum_Not_Denumerable.thy Fri Apr 12 19:48:29 2019 +0200
+++ b/src/HOL/Analysis/Continuum_Not_Denumerable.thy Fri Apr 12 22:09:25 2019 +0200
@@ -11,7 +11,7 @@
"HOL-Library.Countable_Set"
begin
-subsection%unimportant \<open>Abstract\<close>
+subsection\<^marker>\<open>tag unimportant\<close> \<open>Abstract\<close>
text \<open>
The following document presents a proof that the Continuum is uncountable.
@@ -32,7 +32,7 @@
range of \<open>f\<close> by generating a sequence of closed intervals then using the
Nested Interval Property.
\<close>
-text%important \<open>%whitespace\<close>
+text\<^marker>\<open>tag important\<close> \<open>%whitespace\<close>
theorem real_non_denum: "\<nexists>f :: nat \<Rightarrow> real. surj f"
proof
assume "\<exists>f::nat \<Rightarrow> real. surj f"