src/Doc/Prog_Prove/Bool_nat_list.thy

 interchangeably for propositions that have been proved.
 \end{warn}
 \begin{warn}
   Numerals (@{text 0}, @{text 1}, @{text 2}, \dots) and most of the standard
   arithmetic operations (@{text "+"}, @{text "-"}, @{text "*"}, @{text"\<le>"},
-  @{text"<"} etc) are overloaded: they are available
+  @{text"<"}, etc.) are overloaded: they are available
   not just for natural numbers but for other types as well.
   For example, given the goal @{text"x + 0 = x"}, there is nothing to indicate
   that you are talking about natural numbers. Hence Isabelle can only infer
   that @{term x} is of some arbitrary type where @{text 0} and @{text"+"}
   exist. As a consequence, you will be unable to prove the goal.

 that is closer to traditional informal mathematical language and is often
 directly readable.
 
 \subsection{Type \indexed{@{text list}}{list}}
 
-Although lists are already predefined, we define our own copy just for
+Although lists are already predefined, we define our own copy for
 demonstration purposes:
 *}
 (*<*)
 apply(auto)
 done 

 %types of a constructor needs to be enclosed in quotation marks.
 
 \begin{figure}[htbp]
 \begin{alltt}
 \input{MyList.thy}\end{alltt}
-\caption{A Theory of Lists}
+\caption{A theory of lists}
 \label{fig:MyList}
 \index{comment}
 \end{figure}
 
 \subsubsection{Structural Induction for Lists}