# HG changeset patch
# User wenzelm
# Date 1214227608 -7200
# Node ID 6584901d694ccccad86eb1d2df673b8549574bd0
# Parent  5cd16e4df9c2ebb334c05e5d71462a7e9bc90887
updated generated file;

diff -r 5cd16e4df9c2 -r 6584901d694c doc-src/TutorialI/Datatype/document/ABexpr.tex
--- a/doc-src/TutorialI/Datatype/document/ABexpr.tex	Mon Jun 23 15:26:47 2008 +0200
+++ b/doc-src/TutorialI/Datatype/document/ABexpr.tex	Mon Jun 23 15:26:48 2008 +0200
@@ -117,10 +117,9 @@
 %
 \isatagproof
 \isacommand{apply}\isamarkupfalse%
-{\isacharparenleft}induct{\isacharunderscore}tac\ a\ \isakeyword{and}\ b\ rule{\isacharcolon}\ aexp{\isacharunderscore}bexp{\isachardot}induct{\isacharparenright}%
+{\isacharparenleft}induct{\isacharunderscore}tac\ a\ \isakeyword{and}\ b{\isacharparenright}%
 \begin{isamarkuptxt}%
-\noindent Unfortunately, induction needs to be told explicitly which induction rule to use (via \isa{rule{\isacharcolon}}).
-The resulting 8 goals (one for each constructor) are proved in one fell swoop:%
+\noindent The resulting 8 goals (one for each constructor) are proved in one fell swoop:%
 \end{isamarkuptxt}%
 \isamarkuptrue%
 \isacommand{apply}\isamarkupfalse%
@@ -138,7 +137,7 @@
 \[ P@1(x@1)\ \land \dots \land P@n(x@n) \]
 where each variable $x@i$ is of type $\tau@i$. Induction is started by
 \begin{isabelle}
-\isacommand{apply}\isa{{\isacharparenleft}induct{\isacharunderscore}tac} $x@1$ \isacommand{and} \dots\ \isacommand{and} $x@n$ \isa{rule{\isacharcolon}} $\tau@1$\isa{{\isacharunderscore}}\dots\isa{{\isacharunderscore}}$\tau@n$\isa{{\isachardot}induct{\isacharparenright}}
+\isacommand{apply}\isa{{\isacharparenleft}induct{\isacharunderscore}tac} $x@1$ \isacommand{and} \dots\ \isacommand{and} $x@n$\isa{{\isacharparenright}}
 \end{isabelle}
 
 \begin{exercise}
diff -r 5cd16e4df9c2 -r 6584901d694c doc-src/TutorialI/Datatype/document/Nested.tex
--- a/doc-src/TutorialI/Datatype/document/Nested.tex	Mon Jun 23 15:26:47 2008 +0200
+++ b/doc-src/TutorialI/Datatype/document/Nested.tex	Mon Jun 23 15:26:48 2008 +0200
@@ -89,7 +89,7 @@
 %
 \isatagproof
 \isacommand{apply}\isamarkupfalse%
-{\isacharparenleft}induct{\isacharunderscore}tac\ t\ \isakeyword{and}\ ts\ rule{\isacharcolon}\ term{\isachardot}induct{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}\isanewline
+{\isacharparenleft}induct{\isacharunderscore}tac\ t\ \isakeyword{and}\ ts{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}\isanewline
 \isacommand{done}\isamarkupfalse%
 %
 \endisatagproof
diff -r 5cd16e4df9c2 -r 6584901d694c doc-src/TutorialI/Misc/document/AdvancedInd.tex
--- a/doc-src/TutorialI/Misc/document/AdvancedInd.tex	Mon Jun 23 15:26:47 2008 +0200
+++ b/doc-src/TutorialI/Misc/document/AdvancedInd.tex	Mon Jun 23 15:26:48 2008 +0200
@@ -319,12 +319,7 @@
 \begin{quote}
 \isacommand{apply}\isa{{\isacharparenleft}induct{\isacharunderscore}tac} $y@1 \dots y@n$ \isa{rule{\isacharcolon}} $r$\isa{{\isacharparenright}}
 \end{quote}
-where $y@1, \dots, y@n$ are variables in the first subgoal.
-The conclusion of $r$ can even be an (iterated) conjunction of formulae of
-the above form in which case the application is
-\begin{quote}
-\isacommand{apply}\isa{{\isacharparenleft}induct{\isacharunderscore}tac} $y@1 \dots y@n$ \isa{and} \dots\ \isa{and} $z@1 \dots z@m$ \isa{rule{\isacharcolon}} $r$\isa{{\isacharparenright}}
-\end{quote}
+where $y@1, \dots, y@n$ are variables in the conclusion of the first subgoal.
 
 A further useful induction rule is \isa{length{\isacharunderscore}induct},
 induction on the length of a list\indexbold{*length_induct}
diff -r 5cd16e4df9c2 -r 6584901d694c doc-src/TutorialI/Misc/document/pairs.tex
--- a/doc-src/TutorialI/Misc/document/pairs.tex	Mon Jun 23 15:26:47 2008 +0200
+++ b/doc-src/TutorialI/Misc/document/pairs.tex	Mon Jun 23 15:26:48 2008 +0200
@@ -37,7 +37,8 @@
 Products, like type \isa{nat}, are datatypes, which means
 in particular that \isa{induct{\isacharunderscore}tac} and \isa{case{\isacharunderscore}tac} are applicable to
 terms of product type.
-Both replace the term by a pair of variables.
+Both split the term into a number of variables corresponding to the tuple structure
+(up to 7 components).
 \item
 Tuples with more than two or three components become unwieldy;
 records are preferable.
diff -r 5cd16e4df9c2 -r 6584901d694c doc-src/TutorialI/Types/document/Typedefs.tex
--- a/doc-src/TutorialI/Types/document/Typedefs.tex	Mon Jun 23 15:26:47 2008 +0200
+++ b/doc-src/TutorialI/Types/document/Typedefs.tex	Mon Jun 23 15:26:48 2008 +0200
@@ -257,11 +257,11 @@
 \isatagproof
 %
 \begin{isamarkuptxt}%
-\noindent Again this follows easily from a pre-proved general theorem:%
+\noindent Again this follows easily using the induction principle stemming from the type definition:%
 \end{isamarkuptxt}%
 \isamarkuptrue%
 \isacommand{apply}\isamarkupfalse%
-{\isacharparenleft}induct{\isacharunderscore}tac\ x\ rule{\isacharcolon}\ Abs{\isacharunderscore}three{\isacharunderscore}induct{\isacharparenright}%
+{\isacharparenleft}induct{\isacharunderscore}tac\ x{\isacharparenright}%
 \begin{isamarkuptxt}%
 \begin{isabelle}%
 \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}y{\isachardot}\ {\isasymlbrakk}P\ A{\isacharsemicolon}\ P\ B{\isacharsemicolon}\ P\ C{\isacharsemicolon}\ y\ {\isasymin}\ three{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ {\isacharparenleft}Abs{\isacharunderscore}three\ y{\isacharparenright}%