--- 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}
--- 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
--- 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}
--- 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.
--- 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}%