src/HOL/Analysis/Continuum_Not_Denumerable.thy
changeset 68607 67bb59e49834
parent 67968 a5ad4c015d1c
child 69517 dc20f278e8f3
     1.1 --- a/src/HOL/Analysis/Continuum_Not_Denumerable.thy	Mon Jul 09 21:55:40 2018 +0100
     1.2 +++ b/src/HOL/Analysis/Continuum_Not_Denumerable.thy	Tue Jul 10 09:38:35 2018 +0200
     1.3 @@ -33,8 +33,8 @@
     1.4    Nested Interval Property.
     1.5  \<close>
     1.6  
     1.7 -theorem%important real_non_denum: "\<nexists>f :: nat \<Rightarrow> real. surj f"
     1.8 -proof%unimportant
     1.9 +theorem real_non_denum: "\<nexists>f :: nat \<Rightarrow> real. surj f"
    1.10 +proof
    1.11    assume "\<exists>f::nat \<Rightarrow> real. surj f"
    1.12    then obtain f :: "nat \<Rightarrow> real" where "surj f" ..
    1.13