# HG changeset patch
# User wenzelm
# Date 1470675129 -7200
# Node ID d02601840466b35519f3483e4f30ab949a42e1c0
# Parent  1e7c5bbea36dd2dd56705630f8e456de91b9788a
tuned;

diff -r 1e7c5bbea36d -r d02601840466 src/HOL/Library/Continuum_Not_Denumerable.thy
--- a/src/HOL/Library/Continuum_Not_Denumerable.thy	Sun Aug 07 12:10:49 2016 +0200
+++ b/src/HOL/Library/Continuum_Not_Denumerable.thy	Mon Aug 08 18:52:09 2016 +0200
@@ -16,7 +16,7 @@
   It is formalised in the Isabelle/Isar theorem proving system.
 
   \<^bold>\<open>Theorem:\<close> The Continuum \<open>\<real>\<close> is not denumerable. In other words, there does
-  not exist a function \<open>f: \<nat> \<Rightarrow> \<real>\<close> such that f is surjective.
+  not exist a function \<open>f: \<nat> \<Rightarrow> \<real>\<close> such that \<open>f\<close> is surjective.
 
   \<^bold>\<open>Outline:\<close> An elegant informal proof of this result uses Cantor's
   Diagonalisation argument. The proof presented here is not this one.
@@ -28,7 +28,7 @@
   interval is a subset of the last) is non-empty. We then assume a surjective
   function \<open>f: \<nat> \<Rightarrow> \<real>\<close> exists and find a real \<open>x\<close> such that \<open>x\<close> is not in the
   range of \<open>f\<close> by generating a sequence of closed intervals then using the
-  NIP.
+  Nested Interval Property.
 \<close>
 
 theorem real_non_denum: "\<nexists>f :: nat \<Rightarrow> real. surj f"