--- a/doc-src/TutorialI/Inductive/document/Mutual.tex Sun Aug 28 19:42:10 2005 +0200
+++ b/doc-src/TutorialI/Inductive/document/Mutual.tex Sun Aug 28 19:42:19 2005 +0200
@@ -7,6 +7,7 @@
\endisadelimtheory
%
\isatagtheory
+\isamarkupfalse%
%
\endisatagtheory
{\isafoldtheory}%
@@ -14,7 +15,6 @@
\isadelimtheory
%
\endisadelimtheory
-\isamarkuptrue%
%
\isamarkupsubsection{Mutually Inductive Definitions%
}
@@ -25,17 +25,17 @@
by mutual induction. As a trivial example we consider the even and odd
natural numbers:%
\end{isamarkuptext}%
-\isamarkupfalse%
-\isacommand{consts}\ even\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ set{\isachardoublequote}\isanewline
-\ \ \ \ \ \ \ odd\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ set{\isachardoublequote}\isanewline
+\isamarkuptrue%
+\isacommand{consts}\isamarkupfalse%
+\ even\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ set{\isachardoublequoteclose}\isanewline
+\ \ \ \ \ \ \ odd\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ set{\isachardoublequoteclose}\isanewline
\isanewline
-\isamarkupfalse%
-\isacommand{inductive}\ even\ odd\isanewline
+\isacommand{inductive}\isamarkupfalse%
+\ even\ odd\isanewline
\isakeyword{intros}\isanewline
-zero{\isacharcolon}\ \ {\isachardoublequote}{\isadigit{0}}\ {\isasymin}\ even{\isachardoublequote}\isanewline
-evenI{\isacharcolon}\ {\isachardoublequote}n\ {\isasymin}\ odd\ {\isasymLongrightarrow}\ Suc\ n\ {\isasymin}\ even{\isachardoublequote}\isanewline
-oddI{\isacharcolon}\ \ {\isachardoublequote}n\ {\isasymin}\ even\ {\isasymLongrightarrow}\ Suc\ n\ {\isasymin}\ odd{\isachardoublequote}\isamarkuptrue%
-%
+zero{\isacharcolon}\ \ {\isachardoublequoteopen}{\isadigit{0}}\ {\isasymin}\ even{\isachardoublequoteclose}\isanewline
+evenI{\isacharcolon}\ {\isachardoublequoteopen}n\ {\isasymin}\ odd\ {\isasymLongrightarrow}\ Suc\ n\ {\isasymin}\ even{\isachardoublequoteclose}\isanewline
+oddI{\isacharcolon}\ \ {\isachardoublequoteopen}n\ {\isasymin}\ even\ {\isasymLongrightarrow}\ Suc\ n\ {\isasymin}\ odd{\isachardoublequoteclose}%
\begin{isamarkuptext}%
\noindent
The mutually inductive definition of multiple sets is no different from
@@ -50,14 +50,14 @@
If we want to prove that all even numbers are divisible by two, we have to
generalize the statement as follows:%
\end{isamarkuptext}%
-\isamarkupfalse%
-\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}%
+\isamarkuptrue%
+\isacommand{lemma}\isamarkupfalse%
+\ {\isachardoublequoteopen}{\isacharparenleft}m\ {\isasymin}\ even\ {\isasymlongrightarrow}\ {\isadigit{2}}\ dvd\ m{\isacharparenright}\ {\isasymand}\ {\isacharparenleft}n\ {\isasymin}\ odd\ {\isasymlongrightarrow}\ {\isadigit{2}}\ dvd\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
-\isamarkuptrue%
%
\begin{isamarkuptxt}%
\noindent
@@ -65,9 +65,9 @@
it is applied by \isa{rule} rather than \isa{erule} as for ordinary
inductive definitions:%
\end{isamarkuptxt}%
-\isamarkupfalse%
-\isacommand{apply}{\isacharparenleft}rule\ even{\isacharunderscore}odd{\isachardot}induct{\isacharparenright}\isamarkuptrue%
-%
+\isamarkuptrue%
+\isacommand{apply}\isamarkupfalse%
+{\isacharparenleft}rule\ even{\isacharunderscore}odd{\isachardot}induct{\isacharparenright}%
\begin{isamarkuptxt}%
\begin{isabelle}%
\ {\isadigit{1}}{\isachardot}\ {\isadigit{2}}\ dvd\ {\isadigit{0}}\isanewline
@@ -79,6 +79,14 @@
where the same subgoal was encountered before.
We do not show the proof script.%
\end{isamarkuptxt}%
+\isamarkuptrue%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
@@ -92,6 +100,7 @@
\endisadelimtheory
%
\isatagtheory
+\isamarkupfalse%
%
\endisatagtheory
{\isafoldtheory}%