doc-src/TutorialI/ToyList/ToyList.thy

 text{*\noindent
 When Isabelle prints a syntax error message, it refers to the HOL syntax as
 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}
 presented so far, we are ready to prove a few simple theorems. This will
 illustrate not just the basic proof commands but also the typical proof

 *}
 (*<*)
 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
 proof}\indexbold{proof!abandon} (at the shell level type
 \isacommand{oops}\indexbold{*oops}) we start a new proof:

 *}
 (*<*)
 oops
 (*>*)
 
-subsubsection{*Second lemma: @{text"xs @ [] = xs"}*}
+subsubsection{*Second Lemma: @{text"xs @ [] = xs"}*}
 
 text{*
 This time the canonical proof procedure
 *}
 

 \end{isabelle}
 and the missing lemma is associativity of @{text"@"}.
 *}
 (*<*)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
 *}