--- a/doc-src/TutorialI/Inductive/document/Mutual.tex Sun Jan 30 20:48:50 2005 +0100
+++ b/doc-src/TutorialI/Inductive/document/Mutual.tex Tue Feb 01 18:01:57 2005 +0100
@@ -39,27 +39,8 @@
\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%
-\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}%
+\isamarkupfalse%
\isamarkuptrue%
\isamarkupfalse%
\isamarkupfalse%