--- a/doc-src/TutorialI/Misc/document/AdvancedInd.tex Tue Nov 07 18:38:24 2000 +0100
+++ b/doc-src/TutorialI/Misc/document/AdvancedInd.tex Wed Nov 08 14:38:04 2000 +0100
@@ -53,11 +53,11 @@
This means we should prove%
\end{isamarkuptxt}%
\isacommand{lemma}\ hd{\isacharunderscore}rev{\isacharcolon}\ {\isachardoublequote}xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymlongrightarrow}\ hd{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ last\ xs{\isachardoublequote}%
-\begin{isamarkuptext}%
+\begin{isamarkuptxt}%
\noindent
This time, induction leaves us with the following base case
-\begin{isabelle}
-\ 1.\ []\ {\isasymnoteq}\ []\ {\isasymlongrightarrow}\ hd\ (rev\ [])\ =\ last\ []
+\begin{isabelle}%
+\ {\isadigit{1}}{\isachardot}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymlongrightarrow}\ hd\ {\isacharparenleft}rev\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ last\ {\isacharbrackleft}{\isacharbrackright}%
\end{isabelle}
which is trivial, and \isa{auto} finishes the whole proof.
@@ -66,7 +66,7 @@
\isa{hd{\isacharunderscore}rev}, for example because you want to apply it as an
introduction rule, you need to derive it separately, by combining it with
modus ponens:%
-\end{isamarkuptext}%
+\end{isamarkuptxt}%
\isacommand{lemmas}\ hd{\isacharunderscore}revI\ {\isacharequal}\ hd{\isacharunderscore}rev{\isacharbrackleft}THEN\ mp{\isacharbrackright}%
\begin{isamarkuptext}%
\noindent