# HG changeset patch
# User huffman
# Date 1158731074 -7200
# Node ID e95db20977c50e4fc44621bf2fce6889e40b1d18
# Parent  45fe31e72391179dd48093547ed29660749ff702
change section to subsection

diff -r 45fe31e72391 -r e95db20977c5 src/HOL/Hyperreal/Lim.thy
--- 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 =
diff -r 45fe31e72391 -r e95db20977c5 src/HOL/Real/ContNotDenum.thy
--- 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)"