--- a/doc-src/TutorialI/Inductive/document/Mutual.tex Wed May 25 09:03:53 2005 +0200
+++ b/doc-src/TutorialI/Inductive/document/Mutual.tex Wed May 25 09:04:24 2005 +0200
@@ -39,8 +39,27 @@
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}m\ {\isasymin}\ even\ {\isasymlongrightarrow}\ {\isadigit{2}}\ dvd\ m{\isacharparenright}\ {\isasymand}\ {\isacharparenleft}n\ {\isasymin}\ odd\ {\isasymlongrightarrow}\ {\isadigit{2}}\ dvd\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
+%
+\begin{isamarkuptxt}%
+\noindent
+The proof is by rule induction. Because of the form of the induction theorem,
+it is applied by \isa{rule} rather than \isa{erule} as for ordinary
+inductive definitions:%
+\end{isamarkuptxt}%
\isamarkuptrue%
-\isamarkupfalse%
+\isacommand{apply}{\isacharparenleft}rule\ even{\isacharunderscore}odd{\isachardot}induct{\isacharparenright}\isamarkupfalse%
+%
+\begin{isamarkuptxt}%
+\begin{isabelle}%
+\ {\isadigit{1}}{\isachardot}\ {\isadigit{2}}\ dvd\ {\isadigit{0}}\isanewline
+\ {\isadigit{2}}{\isachardot}\ {\isasymAnd}n{\isachardot}\ {\isasymlbrakk}n\ {\isasymin}\ odd{\isacharsemicolon}\ {\isadigit{2}}\ dvd\ Suc\ n{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isadigit{2}}\ dvd\ Suc\ n\isanewline
+\ {\isadigit{3}}{\isachardot}\ {\isasymAnd}n{\isachardot}\ {\isasymlbrakk}n\ {\isasymin}\ Mutual{\isachardot}even{\isacharsemicolon}\ {\isadigit{2}}\ dvd\ n{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isadigit{2}}\ dvd\ Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}%
+\end{isabelle}
+The first two subgoals are proved by simplification and the final one can be
+proved in the same manner as in \S\ref{sec:rule-induction}
+where the same subgoal was encountered before.
+We do not show the proof script.%
+\end{isamarkuptxt}%
\isamarkuptrue%
\isamarkupfalse%
\isamarkupfalse%
@@ -48,7 +67,6 @@
\isamarkupfalse%
\isamarkupfalse%
\isamarkupfalse%
-\isanewline
\isamarkupfalse%
\isamarkupfalse%
\end{isabellebody}%