author nipkow Wed Jun 22 07:54:13 2005 +0200 (2005-06-22) changeset 16522 f718767efd49 parent 16521 ad77345f1db8 child 16523 f8a734dc0fbc
tuned
     1.1 --- a/doc-src/IsarOverview/Isar/Induction.thy	Wed Jun 22 07:54:01 2005 +0200
1.2 +++ b/doc-src/IsarOverview/Isar/Induction.thy	Wed Jun 22 07:54:13 2005 +0200
1.3 @@ -77,7 +77,7 @@
1.4  subsection{*Structural induction*}
1.5
1.6  text{* We start with an inductive proof where both cases are proved automatically: *}
1.7 -lemma "2 * (\<Sum>i::nat < n+1. i) = n*(n+1)"
1.8 +lemma "2 * (\<Sum>i::nat\<le>n. i) = n*(n+1)"
1.9  by (induct n, simp_all)
1.10
1.11  text{*\noindent The constraint @{text"::nat"} is needed because all of
1.12 @@ -86,7 +86,7 @@
1.13  If we want to expose more of the structure of the
1.14  proof, we can use pattern matching to avoid having to repeat the goal
1.15  statement: *}
1.16 -lemma "2 * (\<Sum>i::nat = 0..<n+1. i) = n*(n+1)" (is "?P n")
1.17 +lemma "2 * (\<Sum>i::nat\<le>n. i) = n*(n+1)" (is "?P n")
1.18  proof (induct n)
1.19    show "?P 0" by simp
1.20  next
1.21 @@ -97,7 +97,7 @@
1.22  text{* \noindent We could refine this further to show more of the equational
1.23  proof. Instead we explore the same avenue as for case distinctions:
1.24  introducing context via the \isakeyword{case} command: *}
1.25 -lemma "2 * (\<Sum>i::nat < n+1. i) = n*(n+1)"
1.26 +lemma "2 * (\<Sum>i::nat \<le> n. i) = n*(n+1)"
1.27  proof (induct n)
1.28    case 0 show ?case by simp
1.29  next

     2.1 --- a/doc-src/IsarOverview/Isar/document/Induction.tex	Wed Jun 22 07:54:01 2005 +0200
2.2 +++ b/doc-src/IsarOverview/Isar/document/Induction.tex	Wed Jun 22 07:54:13 2005 +0200
2.3 @@ -127,7 +127,7 @@
2.4  We start with an inductive proof where both cases are proved automatically:%
2.5  \end{isamarkuptext}%
2.6  \isamarkuptrue%
2.9  \isamarkupfalse%
2.10  \isacommand{by}\ {\isacharparenleft}induct\ n{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}\isamarkupfalse%
2.11  %
2.12 @@ -140,7 +140,7 @@
2.13  statement:%
2.14  \end{isamarkuptext}%
2.15  \isamarkuptrue%