author nipkow Mon, 23 May 2005 13:39:45 +0200 changeset 16044 6887e6d12a94 parent 16043 e38b2ec79a2e child 16045 6e2c020eed45
converted back from 0..< to <.
--- a/doc-src/IsarOverview/Isar/Induction.thy	Mon May 23 12:09:30 2005 +0200
+++ b/doc-src/IsarOverview/Isar/Induction.thy	Mon May 23 13:39:45 2005 +0200
@@ -77,7 +77,7 @@
subsection{*Structural induction*}

text{* We start with an inductive proof where both cases are proved automatically: *}
-lemma "2 * (\<Sum>i::nat = 0..<n+1. i) = n*(n+1)"
+lemma "2 * (\<Sum>i::nat < n+1. i) = n*(n+1)"
by (induct n, simp_all)

text{*\noindent The constraint @{text"::nat"} is needed because all of
@@ -97,7 +97,7 @@
text{* \noindent We could refine this further to show more of the equational
proof. Instead we explore the same avenue as for case distinctions:
introducing context via the \isakeyword{case} command: *}
-lemma "2 * (\<Sum>i::nat = 0..<n+1. i) = n*(n+1)"
+lemma "2 * (\<Sum>i::nat < n+1. i) = n*(n+1)"
proof (induct n)
case 0 show ?case by simp
next
--- a/doc-src/IsarOverview/Isar/document/Induction.tex	Mon May 23 12:09:30 2005 +0200
+++ b/doc-src/IsarOverview/Isar/document/Induction.tex	Mon May 23 13:39:45 2005 +0200
@@ -115,7 +115,7 @@
We start with an inductive proof where both cases are proved automatically:%
\end{isamarkuptext}%
\isamarkuptrue%
\isamarkupfalse%