--- a/src/HOL/ex/HarmonicSeries.thy Tue Jan 16 09:12:16 2018 +0100
+++ b/src/HOL/ex/HarmonicSeries.thy Tue Jan 16 09:30:00 2018 +0100
@@ -138,7 +138,7 @@
have ant: "0 < Suc M" by fact
{
have suc: "?LHS (Suc M) = ?RHS (Suc M)"
- proof cases \<comment> "show that LHS = c and RHS = c, and thus LHS = RHS"
+ proof cases \<comment> \<open>show that LHS = c and RHS = c, and thus LHS = RHS\<close>
assume mz: "M=0"
{
then have
@@ -274,8 +274,8 @@
theorem DivergenceOfHarmonicSeries:
shows "\<not>summable (\<lambda>n. 1/real (Suc n))"
(is "\<not>summable ?f")
-proof \<comment> "by contradiction"
- let ?s = "suminf ?f" \<comment> "let ?s equal the sum of the harmonic series"
+proof \<comment> \<open>by contradiction\<close>
+ let ?s = "suminf ?f" \<comment> \<open>let ?s equal the sum of the harmonic series\<close>
assume sf: "summable ?f"
then obtain n::nat where ndef: "n = nat \<lceil>2 * ?s\<rceil>" by simp
then have ngt: "1 + real n/2 > ?s" by linarith