Turned sections into subsections (better document structure).
authorwebertj
Sat, 07 Nov 2009 18:53:29 +0000
changeset 33509 29e4cf2c4ea3
parent 33437 c8bc8dc5869f
child 33510 e744ad2d0393
Turned sections into subsections (better document structure).
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)"