diff -r a5d3730043c2 -r 7d5ad23b8245 src/Doc/ProgProve/Bool_nat_list.thy
--- a/src/Doc/ProgProve/Bool_nat_list.thy	Mon Jun 10 08:39:48 2013 -0400
+++ b/src/Doc/ProgProve/Bool_nat_list.thy	Mon Jun 10 16:04:18 2013 +0200
@@ -109,7 +109,7 @@
   overloaded.
 \end{warn}
 
-\subsubsection{An informal proof}
+\subsubsection{An Informal Proof}
 
 Above we gave some terse informal explanation of the proof of
 @{prop"add m 0 = m"}. A more detailed informal exposition of the lemma
@@ -335,7 +335,7 @@
 Finally the proofs of @{thm[source] rev_app} and @{thm[source] rev_rev}
 succeed, too.
 
-\subsubsection{Another informal proof}
+\subsubsection{Another Informal Proof}
 
 Here is the informal proof of associativity of @{const app}
 corresponding to the Isabelle proof above.
@@ -377,7 +377,7 @@
 @{text s} is @{term"app (app Nil ys) zs"}, @{text t} is @{term"app Nil (app
 ys zs)"}, and @{text u} is @{term"app ys zs"}.
 
-\subsection{Predefined lists}
+\subsection{Predefined Lists}
 \label{sec:predeflists}
 
 Isabelle's predefined lists are the same as the ones above, but with