# HG changeset patch
# User webertj
# Date 1257620009 0
# Node ID 29e4cf2c4ea361c06252e80f35ff9d552798f427
# Parent  c8bc8dc5869ffe574f00835a06f8e39130ec9610
Turned sections into subsections (better document structure).

diff -r c8bc8dc5869f -r 29e4cf2c4ea3 src/HOL/ex/HarmonicSeries.thy
--- a/src/HOL/ex/HarmonicSeries.thy	Wed Nov 04 17:17:30 2009 +0100
+++ b/src/HOL/ex/HarmonicSeries.thy	Sat Nov 07 18:53:29 2009 +0000
@@ -8,7 +8,7 @@
 imports Complex_Main
 begin
 
-section {* Abstract *}
+subsection {* Abstract *}
 
 text {* The following document presents a proof of the Divergence of
 Harmonic Series theorem formalised in the Isabelle/Isar theorem
@@ -35,7 +35,7 @@
   QED.
 *}
 
-section {* Formal Proof *}
+subsection {* Formal Proof *}
 
 lemma two_pow_sub:
   "0 < m \<Longrightarrow> (2::nat)^m - 2^(m - 1) = 2^(m - 1)"