# HG changeset patch
# User nipkow
# Date 1213273225 -7200
# Node ID a99747ccba87b1c7284d7f051d2828320ec33f3e
# Parent  968a1450ae3577edfc882a1531121be3de74e337
typo

diff -r 968a1450ae35 -r a99747ccba87 doc-src/TutorialI/Fun/document/fun0.tex
--- a/doc-src/TutorialI/Fun/document/fun0.tex	Thu Jun 12 14:20:07 2008 +0200
+++ b/doc-src/TutorialI/Fun/document/fun0.tex	Thu Jun 12 14:20:25 2008 +0200
@@ -322,7 +322,7 @@
 \isacommand{apply}\isa{{\isacharparenleft}induct{\isacharunderscore}tac} $x@1 \dots x@n$ \isa{rule{\isacharcolon}} $f$\isa{{\isachardot}induct{\isacharparenright}}
 \end{quote}\index{*induct_tac (method)}%
 where $x@1~\dots~x@n$ is a list of free variables in the subgoal and $f$ the
-name of a function that takes an $n$ arguments. Usually the subgoal will
+name of a function that takes $n$ arguments. Usually the subgoal will
 contain the term $f x@1 \dots x@n$ but this need not be the case. The
 induction rules do not mention $f$ at all. Here is \isa{sep{\isachardot}induct}:
 \begin{isabelle}
diff -r 968a1450ae35 -r a99747ccba87 doc-src/TutorialI/Fun/fun0.thy
--- a/doc-src/TutorialI/Fun/fun0.thy	Thu Jun 12 14:20:07 2008 +0200
+++ b/doc-src/TutorialI/Fun/fun0.thy	Thu Jun 12 14:20:25 2008 +0200
@@ -239,7 +239,7 @@
 \isacommand{apply}@{text"(induct_tac"} $x@1 \dots x@n$ @{text"rule:"} $f$@{text".induct)"}
 \end{quote}\index{*induct_tac (method)}%
 where $x@1~\dots~x@n$ is a list of free variables in the subgoal and $f$ the
-name of a function that takes an $n$ arguments. Usually the subgoal will
+name of a function that takes $n$ arguments. Usually the subgoal will
 contain the term $f x@1 \dots x@n$ but this need not be the case. The
 induction rules do not mention $f$ at all. Here is @{thm[source]sep.induct}:
 \begin{isabelle}
diff -r 968a1450ae35 -r a99747ccba87 doc-src/TutorialI/Inductive/AB.thy
--- a/doc-src/TutorialI/Inductive/AB.thy	Thu Jun 12 14:20:07 2008 +0200
+++ b/doc-src/TutorialI/Inductive/AB.thy	Thu Jun 12 14:20:25 2008 +0200
@@ -60,7 +60,7 @@
 a}'s and @{term b}'s. Since the definition of @{term S} is by mutual
 induction, so is the proof: we show at the same time that all words in
 @{term A} contain one more @{term a} than @{term b} and all words in @{term
-B} contains one more @{term b} than @{term a}.
+B} contain one more @{term b} than @{term a}.
 *}
 
 lemma correctness:
@@ -199,13 +199,14 @@
 *}
 
 apply(induct_tac w rule: length_induct)
-(*<*)apply(rename_tac w)(*>*)
+apply(rename_tac w)
 
 txt{*\noindent
 The @{text rule} parameter tells @{text induct_tac} explicitly which induction
 rule to use. For details see \S\ref{sec:complete-ind} below.
 In this case the result is that we may assume the lemma already
-holds for all words shorter than @{term w}.
+holds for all words shorter than @{term w}. Because the induction step renames
+the induction variable we rename it back to @{text w}.
 
 The proof continues with a case distinction on @{term w},
 on whether @{term w} is empty or not.
diff -r 968a1450ae35 -r a99747ccba87 doc-src/TutorialI/Inductive/Advanced.thy
--- a/doc-src/TutorialI/Inductive/Advanced.thy	Thu Jun 12 14:20:07 2008 +0200
+++ b/doc-src/TutorialI/Inductive/Advanced.thy	Thu Jun 12 14:20:25 2008 +0200
@@ -234,8 +234,8 @@
 apply (erule well_formed_gterm'.induct)
 (*>*)
 txt {*
-The proof script is identical, but the subgoal after applying induction may
-be surprising:
+The proof script is virtually identical,
+but the subgoal after applying induction may be surprising:
 @{subgoals[display,indent=0,margin=65]}
 The induction hypothesis contains an application of @{term lists}.  Using a
 monotone function in the inductive definition always has this effect.  The
diff -r 968a1450ae35 -r a99747ccba87 doc-src/TutorialI/Inductive/document/AB.tex
--- a/doc-src/TutorialI/Inductive/document/AB.tex	Thu Jun 12 14:20:07 2008 +0200
+++ b/doc-src/TutorialI/Inductive/document/AB.tex	Thu Jun 12 14:20:25 2008 +0200
@@ -93,7 +93,7 @@
 \noindent
 First we show that all words in \isa{S} contain the same number of \isa{a}'s and \isa{b}'s. Since the definition of \isa{S} is by mutual
 induction, so is the proof: we show at the same time that all words in
-\isa{A} contain one more \isa{a} than \isa{b} and all words in \isa{B} contains one more \isa{b} than \isa{a}.%
+\isa{A} contain one more \isa{a} than \isa{b} and all words in \isa{B} contain one more \isa{b} than \isa{a}.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 \isacommand{lemma}\isamarkupfalse%
@@ -303,13 +303,16 @@
 \end{isamarkuptxt}%
 \isamarkuptrue%
 \isacommand{apply}\isamarkupfalse%
-{\isacharparenleft}induct{\isacharunderscore}tac\ w\ rule{\isacharcolon}\ length{\isacharunderscore}induct{\isacharparenright}%
+{\isacharparenleft}induct{\isacharunderscore}tac\ w\ rule{\isacharcolon}\ length{\isacharunderscore}induct{\isacharparenright}\isanewline
+\isacommand{apply}\isamarkupfalse%
+{\isacharparenleft}rename{\isacharunderscore}tac\ w{\isacharparenright}%
 \begin{isamarkuptxt}%
 \noindent
 The \isa{rule} parameter tells \isa{induct{\isacharunderscore}tac} explicitly which induction
 rule to use. For details see \S\ref{sec:complete-ind} below.
 In this case the result is that we may assume the lemma already
-holds for all words shorter than \isa{w}.
+holds for all words shorter than \isa{w}. Because the induction step renames
+the induction variable we rename it back to \isa{w}.
 
 The proof continues with a case distinction on \isa{w},
 on whether \isa{w} is empty or not.%
diff -r 968a1450ae35 -r a99747ccba87 doc-src/TutorialI/Inductive/document/Advanced.tex
--- a/doc-src/TutorialI/Inductive/document/Advanced.tex	Thu Jun 12 14:20:07 2008 +0200
+++ b/doc-src/TutorialI/Inductive/document/Advanced.tex	Thu Jun 12 14:20:25 2008 +0200
@@ -346,8 +346,8 @@
 \isatagproof
 %
 \begin{isamarkuptxt}%
-The proof script is identical, but the subgoal after applying induction may
-be surprising:
+The proof script is virtually identical,
+but the subgoal after applying induction may be surprising:
 \begin{isabelle}%
 \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x\ args\ f{\isachardot}\isanewline
 \isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymlbrakk}args\isanewline
diff -r 968a1450ae35 -r a99747ccba87 doc-src/TutorialI/Rules/rules.tex
--- a/doc-src/TutorialI/Rules/rules.tex	Thu Jun 12 14:20:07 2008 +0200
+++ b/doc-src/TutorialI/Rules/rules.tex	Thu Jun 12 14:20:25 2008 +0200
@@ -220,7 +220,7 @@
 The result of this proof is a new inference rule \isa{disj_swap}, which is neither 
 an introduction nor an elimination rule, but which might 
 be useful.  We can use it to replace any goal of the form $Q\disj P$
-by a one of the form $P\disj Q$.%
+by one of the form $P\disj Q$.%
 \index{elimination rules|)}
 
 
@@ -515,16 +515,15 @@
 \begin{isabelle}
 \isacommand{lemma}\ "(P\ \isasymor\ Q)\ \isasymand\ R\
 \isasymLongrightarrow\ P\ \isasymor\ (Q\ \isasymand\ R)"\isanewline
-\isacommand{apply}\ (intro\ disjCI\ conjI)\isanewline
+\isacommand{apply}\ (rule\ disjCI)\isanewline
 \isacommand{apply}\ (elim\ conjE\ disjE)\isanewline
 \ \isacommand{apply}\ assumption
 \isanewline
 \isacommand{by}\ (erule\ contrapos_np,\ rule\ conjI)
 \end{isabelle}
 %
-The first proof step uses \isa{intro} to apply
-the introduction rules \isa{disjCI} and \isa{conjI}.  The resulting
-subgoal has the negative assumption 
+The first proof step to applies the introduction rules \isa{disjCI}.
+The resulting subgoal has the negative assumption 
 \hbox{\isa{\isasymnot(Q\ \isasymand\ R)}}.  
 
 \begin{isabelle}
@@ -901,11 +900,11 @@
 arbitrary, since it has not been assumed to satisfy any special conditions. 
 Isabelle's  underlying formalism, called the
 \bfindex{meta-logic}, eliminates the  need for English.  It provides its own
-universal quantifier (\isasymAnd) to express the notion of an arbitrary value.  We
-have already seen  another symbol of the meta-logic, namely
-\isa\isasymLongrightarrow, which expresses  inference rules and the treatment of
-assumptions. The only other  symbol in the meta-logic is \isa\isasymequiv, which
-can be used to define constants.
+universal quantifier (\isasymAnd) to express the notion of an arbitrary value.
+We have already seen  another operator of the meta-logic, namely
+\isa\isasymLongrightarrow, which expresses  inference rules and the treatment
+of assumptions. The only other operator in the meta-logic is \isa\isasymequiv,
+which can be used to define constants.
 
 \subsection{The Universal Introduction Rule}