--- a/doc-src/TutorialI/ToyList/document/ToyList.tex Fri Jan 12 16:05:12 2001 +0100
+++ b/doc-src/TutorialI/ToyList/document/ToyList.tex Fri Jan 12 16:07:20 2001 +0100
@@ -104,7 +104,7 @@
the \bfindex{inner syntax} and the enclosing theory language as the \bfindex{outer syntax}.
-\section{An introductory proof}
+\section{An Introductory Proof}
\label{sec:intro-proof}
Assuming you have input the declarations and definitions of \texttt{ToyList}
@@ -210,7 +210,7 @@
In order to simplify this subgoal further, a lemma suggests itself.%
\end{isamarkuptxt}%
%
-\isamarkupsubsubsection{First lemma: \isa{rev{\isacharparenleft}xs\ {\isacharat}\ ys{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}rev\ ys{\isacharparenright}\ {\isacharat}\ {\isacharparenleft}rev\ xs{\isacharparenright}}%
+\isamarkupsubsubsection{First Lemma: \isa{rev{\isacharparenleft}xs\ {\isacharat}\ ys{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}rev\ ys{\isacharparenright}\ {\isacharat}\ {\isacharparenleft}rev\ xs{\isacharparenright}}%
}
%
\begin{isamarkuptext}%
@@ -245,7 +245,7 @@
embarking on the proof of a lemma usually remains implicit.%
\end{isamarkuptxt}%
%
-\isamarkupsubsubsection{Second lemma: \isa{xs\ {\isacharat}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ xs}%
+\isamarkupsubsubsection{Second Lemma: \isa{xs\ {\isacharat}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ xs}%
}
%
\begin{isamarkuptext}%
@@ -300,7 +300,7 @@
and the missing lemma is associativity of \isa{{\isacharat}}.%
\end{isamarkuptxt}%
%
-\isamarkupsubsubsection{Third lemma: \isa{{\isacharparenleft}xs\ {\isacharat}\ ys{\isacharparenright}\ {\isacharat}\ zs\ {\isacharequal}\ xs\ {\isacharat}\ {\isacharparenleft}ys\ {\isacharat}\ zs{\isacharparenright}}%
+\isamarkupsubsubsection{Third Lemma: \isa{{\isacharparenleft}xs\ {\isacharat}\ ys{\isacharparenright}\ {\isacharat}\ zs\ {\isacharequal}\ xs\ {\isacharat}\ {\isacharparenleft}ys\ {\isacharat}\ zs{\isacharparenright}}%
}
%
\begin{isamarkuptext}%