# HG changeset patch
# User nipkow
# Date 1119419653 -7200
# Node ID f718767efd49f63597797ae65eaf9ea7735efbde
# Parent  ad77345f1db8983eef0817e56a190cd1830b064a
tuned

diff -r ad77345f1db8 -r f718767efd49 doc-src/IsarOverview/Isar/Induction.thy
--- a/doc-src/IsarOverview/Isar/Induction.thy	Wed Jun 22 07:54:01 2005 +0200
+++ b/doc-src/IsarOverview/Isar/Induction.thy	Wed Jun 22 07:54:13 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 < n+1. i) = n*(n+1)"
+lemma "2 * (\<Sum>i::nat\<le>n. i) = n*(n+1)"
 by (induct n, simp_all)
 
 text{*\noindent The constraint @{text"::nat"} is needed because all of
@@ -86,7 +86,7 @@
 If we want to expose more of the structure of the
 proof, we can use pattern matching to avoid having to repeat the goal
 statement: *}
-lemma "2 * (\<Sum>i::nat = 0..<n+1. i) = n*(n+1)" (is "?P n")
+lemma "2 * (\<Sum>i::nat\<le>n. i) = n*(n+1)" (is "?P n")
 proof (induct n)
   show "?P 0" by simp
 next
@@ -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 < n+1. i) = n*(n+1)"
+lemma "2 * (\<Sum>i::nat \<le> n. i) = n*(n+1)"
 proof (induct n)
   case 0 show ?case by simp
 next
diff -r ad77345f1db8 -r f718767efd49 doc-src/IsarOverview/Isar/document/Induction.tex
--- a/doc-src/IsarOverview/Isar/document/Induction.tex	Wed Jun 22 07:54:01 2005 +0200
+++ b/doc-src/IsarOverview/Isar/document/Induction.tex	Wed Jun 22 07:54:13 2005 +0200
@@ -127,7 +127,7 @@
 We start with an inductive proof where both cases are proved automatically:%
 \end{isamarkuptext}%
 \isamarkuptrue%
-\isacommand{lemma}\ {\isachardoublequote}{\isadigit{2}}\ {\isacharasterisk}\ {\isacharparenleft}{\isasymSum}i{\isacharcolon}{\isacharcolon}nat\ {\isacharless}\ n{\isacharplus}{\isadigit{1}}{\isachardot}\ i{\isacharparenright}\ {\isacharequal}\ n{\isacharasterisk}{\isacharparenleft}n{\isacharplus}{\isadigit{1}}{\isacharparenright}{\isachardoublequote}\isanewline
+\isacommand{lemma}\ {\isachardoublequote}{\isadigit{2}}\ {\isacharasterisk}\ {\isacharparenleft}{\isasymSum}i{\isacharcolon}{\isacharcolon}nat{\isasymle}n{\isachardot}\ i{\isacharparenright}\ {\isacharequal}\ n{\isacharasterisk}{\isacharparenleft}n{\isacharplus}{\isadigit{1}}{\isacharparenright}{\isachardoublequote}\isanewline
 \isamarkupfalse%
 \isacommand{by}\ {\isacharparenleft}induct\ n{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}\isamarkupfalse%
 %
@@ -140,7 +140,7 @@
 statement:%
 \end{isamarkuptext}%
 \isamarkuptrue%
-\isacommand{lemma}\ {\isachardoublequote}{\isadigit{2}}\ {\isacharasterisk}\ {\isacharparenleft}{\isasymSum}i{\isacharcolon}{\isacharcolon}nat\ {\isacharequal}\ {\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}n{\isacharplus}{\isadigit{1}}{\isachardot}\ i{\isacharparenright}\ {\isacharequal}\ n{\isacharasterisk}{\isacharparenleft}n{\isacharplus}{\isadigit{1}}{\isacharparenright}{\isachardoublequote}\ {\isacharparenleft}\isakeyword{is}\ {\isachardoublequote}{\isacharquery}P\ n{\isachardoublequote}{\isacharparenright}\isanewline
+\isacommand{lemma}\ {\isachardoublequote}{\isadigit{2}}\ {\isacharasterisk}\ {\isacharparenleft}{\isasymSum}i{\isacharcolon}{\isacharcolon}nat{\isasymle}n{\isachardot}\ i{\isacharparenright}\ {\isacharequal}\ n{\isacharasterisk}{\isacharparenleft}n{\isacharplus}{\isadigit{1}}{\isacharparenright}{\isachardoublequote}\ {\isacharparenleft}\isakeyword{is}\ {\isachardoublequote}{\isacharquery}P\ n{\isachardoublequote}{\isacharparenright}\isanewline
 \isamarkupfalse%
 \isacommand{proof}\ {\isacharparenleft}induct\ n{\isacharparenright}\isanewline
 \ \ \isamarkupfalse%
@@ -163,7 +163,7 @@
 introducing context via the \isakeyword{case} command:%
 \end{isamarkuptext}%
 \isamarkuptrue%
-\isacommand{lemma}\ {\isachardoublequote}{\isadigit{2}}\ {\isacharasterisk}\ {\isacharparenleft}{\isasymSum}i{\isacharcolon}{\isacharcolon}nat\ {\isacharless}\ n{\isacharplus}{\isadigit{1}}{\isachardot}\ i{\isacharparenright}\ {\isacharequal}\ n{\isacharasterisk}{\isacharparenleft}n{\isacharplus}{\isadigit{1}}{\isacharparenright}{\isachardoublequote}\isanewline
+\isacommand{lemma}\ {\isachardoublequote}{\isadigit{2}}\ {\isacharasterisk}\ {\isacharparenleft}{\isasymSum}i{\isacharcolon}{\isacharcolon}nat\ {\isasymle}\ n{\isachardot}\ i{\isacharparenright}\ {\isacharequal}\ n{\isacharasterisk}{\isacharparenleft}n{\isacharplus}{\isadigit{1}}{\isacharparenright}{\isachardoublequote}\isanewline
 \isamarkupfalse%
 \isacommand{proof}\ {\isacharparenleft}induct\ n{\isacharparenright}\isanewline
 \ \ \isamarkupfalse%