--- 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)"