--- a/src/HOL/Analysis/Continuum_Not_Denumerable.thy Mon Jul 09 21:55:40 2018 +0100
+++ b/src/HOL/Analysis/Continuum_Not_Denumerable.thy Tue Jul 10 09:38:35 2018 +0200
@@ -33,8 +33,8 @@
Nested Interval Property.
\<close>
-theorem%important real_non_denum: "\<nexists>f :: nat \<Rightarrow> real. surj f"
-proof%unimportant
+theorem real_non_denum: "\<nexists>f :: nat \<Rightarrow> real. surj f"
+proof
assume "\<exists>f::nat \<Rightarrow> real. surj f"
then obtain f :: "nat \<Rightarrow> real" where "surj f" ..