diff -r 2995639c6a09 -r 90695f46440b doc-src/TutorialI/fp.tex
--- a/doc-src/TutorialI/fp.tex	Fri Jan 12 16:28:14 2001 +0100
+++ b/doc-src/TutorialI/fp.tex	Fri Jan 12 16:32:01 2001 +0100
@@ -12,7 +12,7 @@
 goes well beyond what can be expressed as a program. However, for the time
 being we concentrate on the computable.
 
-\section{An introductory theory}
+\section{An Introductory Theory}
 \label{sec:intro-theory}
 
 Functional programming needs datatypes and functions. Both of them can be
@@ -55,7 +55,7 @@
 \end{itemize}
 
 
-\section{Some helpful commands}
+\section{Some Helpful Commands}
 \label{sec:commands-and-hints}
 
 This section discusses a few basic commands for manipulating the proof state
@@ -167,7 +167,7 @@
 always use HOL's predefined lists.
 
 
-\subsection{The general format}
+\subsection{The General Format}
 \label{sec:general-datatype}
 
 The general HOL \isacommand{datatype} definition is of the form
@@ -198,7 +198,7 @@
 Isabelle will always show \isa{size} on lists as \isa{length}.
 
 
-\subsection{Primitive recursion}
+\subsection{Primitive Recursion}
 
 Functions on datatypes are usually defined by recursion. In fact, most of the
 time they are defined by what is called \bfindex{primitive recursion}.
@@ -221,10 +221,10 @@
 
 \input{Ifexpr/document/Ifexpr.tex}
 
-\section{Some basic types}
+\section{Some Basic Types}
 
 
-\subsection{Natural numbers}
+\subsection{Natural Numbers}
 \label{sec:nat}
 \index{arithmetic|(}
 
@@ -251,7 +251,7 @@
 definitions.
 
 
-\subsection{Type synonyms}
+\subsection{Type Synonyms}
 \indexbold{type synonym}
 
 Type synonyms are similar to those found in ML\@. Their syntax is fairly self
@@ -302,7 +302,7 @@
 section as well, in particular in order to understand what happened if things
 do not simplify as expected.
 
-\subsubsection{What is simplification}
+\subsubsection{What is Simplification?}
 
 In its most basic form, simplification means repeated application of
 equations from left to right. For example, taking the rules for \isa{\at}
@@ -329,7 +329,7 @@
 \input{CodeGen/document/CodeGen.tex}
 
 
-\section{Advanced datatypes}
+\section{Advanced Datatypes}
 \label{sec:advanced-datatypes}
 \index{*datatype|(}
 \index{*primrec|(}
@@ -337,18 +337,18 @@
 
 This section presents advanced forms of \isacommand{datatype}s.
 
-\subsection{Mutual recursion}
+\subsection{Mutual Recursion}
 \label{sec:datatype-mut-rec}
 
 \input{Datatype/document/ABexpr.tex}
 
-\subsection{Nested recursion}
+\subsection{Nested Recursion}
 \label{sec:nested-datatype}
 
 {\makeatother\input{Datatype/document/Nested.tex}}
 
 
-\subsection{The limits of nested recursion}
+\subsection{The Limits of Nested Recursion}
 
 How far can we push nested recursion? By the unfolding argument above, we can
 reduce nested to mutual recursion provided the nested recursion only involves
@@ -387,7 +387,7 @@
 \index{*primrec|)}
 \index{*datatype|)}
 
-\subsection{Case study: Tries}
+\subsection{Case Study: Tries}
 \label{sec:Trie}
 
 Tries are a classic search tree data structure~\cite{Knuth3-75} for fast
@@ -455,7 +455,7 @@
   deletion, if possible.
 \end{exercise}
 
-\section{Total recursive functions}
+\section{Total Recursive Functions}
 \label{sec:recdef}
 \index{*recdef|(}
 
@@ -467,15 +467,15 @@
 supplied) sense. In this section we ristrict ourselves to measure functions;
 more advanced termination proofs are discussed in {\S}\ref{sec:beyond-measure}.
 
-\subsection{Defining recursive functions}
+\subsection{Defining Recursive Functions}
 \label{sec:recdef-examples}
 \input{Recdef/document/examples.tex}
 
-\subsection{Proving termination}
+\subsection{Proving Termination}
 
 \input{Recdef/document/termination.tex}
 
-\subsection{Simplification with recdef}
+\subsection{Simplification with Recdef}
 \label{sec:recdef-simplification}
 
 \input{Recdef/document/simplification.tex}