--- a/doc-src/TutorialI/ToyList/ToyList.thy Fri Jan 12 16:28:14 2001 +0100
+++ b/doc-src/TutorialI/ToyList/ToyList.thy Fri Jan 12 16:32:01 2001 +0100
@@ -107,7 +107,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}
@@ -220,7 +220,7 @@
oops
(*>*)
-subsubsection{*First lemma: @{text"rev(xs @ ys) = (rev ys) @ (rev xs)"}*}
+subsubsection{*First Lemma: @{text"rev(xs @ ys) = (rev ys) @ (rev xs)"}*}
text{*
After abandoning the above proof attempt\indexbold{abandon
@@ -259,7 +259,7 @@
oops
(*>*)
-subsubsection{*Second lemma: @{text"xs @ [] = xs"}*}
+subsubsection{*Second Lemma: @{text"xs @ [] = xs"}*}
text{*
This time the canonical proof procedure
@@ -312,7 +312,7 @@
*}
(*<*)oops(*>*)
-subsubsection{*Third lemma: @{text"(xs @ ys) @ zs = xs @ (ys @ zs)"}*}
+subsubsection{*Third Lemma: @{text"(xs @ ys) @ zs = xs @ (ys @ zs)"}*}
text{*
Abandoning the previous proof, the canonical proof procedure