--- a/doc-src/TutorialI/Recdef/document/Induction.tex Sun Aug 28 19:42:10 2005 +0200
+++ b/doc-src/TutorialI/Recdef/document/Induction.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%
%
\begin{isamarkuptext}%
Assuming we have defined our function such that Isabelle could prove
@@ -32,14 +32,14 @@
for all recursive calls on the right-hand side. Here is a simple example
involving the predefined \isa{map} functional on lists:%
\end{isamarkuptext}%
-\isamarkupfalse%
-\isacommand{lemma}\ {\isachardoublequote}map\ f\ {\isacharparenleft}sep{\isacharparenleft}x{\isacharcomma}xs{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ sep{\isacharparenleft}f\ x{\isacharcomma}\ map\ f\ xs{\isacharparenright}{\isachardoublequote}%
+\isamarkuptrue%
+\isacommand{lemma}\isamarkupfalse%
+\ {\isachardoublequoteopen}map\ f\ {\isacharparenleft}sep{\isacharparenleft}x{\isacharcomma}xs{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ sep{\isacharparenleft}f\ x{\isacharcomma}\ map\ f\ xs{\isacharparenright}{\isachardoublequoteclose}%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
-\isamarkuptrue%
%
\begin{isamarkuptxt}%
\noindent
@@ -47,9 +47,9 @@
is the result of applying \isa{f} to all elements of \isa{xs}. We prove
this lemma by recursion induction over \isa{sep}:%
\end{isamarkuptxt}%
-\isamarkupfalse%
-\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ x\ xs\ rule{\isacharcolon}\ sep{\isachardot}induct{\isacharparenright}\isamarkuptrue%
-%
+\isamarkuptrue%
+\isacommand{apply}\isamarkupfalse%
+{\isacharparenleft}induct{\isacharunderscore}tac\ x\ xs\ rule{\isacharcolon}\ sep{\isachardot}induct{\isacharparenright}%
\begin{isamarkuptxt}%
\noindent
The resulting proof state has three subgoals corresponding to the three
@@ -63,17 +63,17 @@
\end{isabelle}
The rest is pure simplification:%
\end{isamarkuptxt}%
-\isamarkupfalse%
-\isacommand{apply}\ simp{\isacharunderscore}all\isanewline
-\isamarkupfalse%
-\isacommand{done}%
+\isamarkuptrue%
+\isacommand{apply}\isamarkupfalse%
+\ simp{\isacharunderscore}all\isanewline
+\isacommand{done}\isamarkupfalse%
+%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
%
\endisadelimproof
-\isamarkuptrue%
%
\begin{isamarkuptext}%
Try proving the above lemma by structural induction, and you find that you
@@ -101,12 +101,14 @@
The final case has an induction hypothesis: you may assume that \isa{P}
holds for the tail of that list.%
\end{isamarkuptext}%
+\isamarkuptrue%
%
\isadelimtheory
%
\endisadelimtheory
%
\isatagtheory
+\isamarkupfalse%
%
\endisatagtheory
{\isafoldtheory}%