--- a/src/HOL/Hyperreal/Lim.thy Wed Sep 20 07:42:12 2006 +0200
+++ b/src/HOL/Hyperreal/Lim.thy Wed Sep 20 07:44:34 2006 +0200
@@ -74,7 +74,7 @@
-section{*Some Purely Standard Proofs*}
+subsection{*Some Purely Standard Proofs*}
lemma LIM_eq:
"f -- a --> L =
--- a/src/HOL/Real/ContNotDenum.thy Wed Sep 20 07:42:12 2006 +0200
+++ b/src/HOL/Real/ContNotDenum.thy Wed Sep 20 07:44:34 2006 +0200
@@ -9,7 +9,7 @@
imports RComplete
begin
-section {* Abstract *}
+subsection {* Abstract *}
text {* The following document presents a proof that the Continuum is
uncountable. It is formalised in the Isabelle/Isar theorem proving
@@ -30,17 +30,17 @@
"\<nat>\<Rightarrow>\<real>"} exists and find a real x such that x is not in the range of f
by generating a sequence of closed intervals then using the NIP. *}
-section {* Closed Intervals *}
+subsection {* Closed Intervals *}
text {* This section formalises some properties of closed intervals. *}
-subsection {* Definition *}
+subsubsection {* Definition *}
definition
closed_int :: "real \<Rightarrow> real \<Rightarrow> real set"
"closed_int x y = {z. x \<le> z \<and> z \<le> y}"
-subsection {* Properties *}
+subsubsection {* Properties *}
lemma closed_int_subset:
assumes xy: "x1 \<ge> x0" "y1 \<le> y0"
@@ -99,7 +99,7 @@
qed
-section {* Nested Interval Property *}
+subsection {* Nested Interval Property *}
theorem NIP:
fixes f::"nat \<Rightarrow> real set"
@@ -313,7 +313,7 @@
thus ?thesis by auto
qed
-section {* Generating the intervals *}
+subsection {* Generating the intervals *}
subsubsection {* Existence of non-singleton closed intervals *}
@@ -560,7 +560,7 @@
qed
-section {* Final Theorem *}
+subsection {* Final Theorem *}
theorem real_non_denum:
shows "\<not> (\<exists>f::nat\<Rightarrow>real. surj f)"