--- a/doc-src/TutorialI/Advanced/advanced.tex Mon Mar 19 13:28:06 2001 +0100
+++ b/doc-src/TutorialI/Advanced/advanced.tex Mon Mar 19 17:25:42 2001 +0100
@@ -9,7 +9,7 @@
\input{Advanced/document/simp.tex}
-\section{Advanced forms of recursion}
+\section{Advanced Forms of Recursion}
\index{*recdef|(}
The purpose of this section is to introduce advanced forms of
@@ -27,23 +27,23 @@
proof time. In HOL you may have to work hard to define a function, but proofs
can then proceed unencumbered by worries about undefinedness.
-\subsection{Beyond measure}
+\subsection{Beyond Measure}
\label{sec:beyond-measure}
\input{Advanced/document/WFrec.tex}
-\subsection{Recursion over nested datatypes}
+\subsection{Recursion Over Nested Datatypes}
\label{sec:nested-recdef}
\input{Recdef/document/Nested0.tex}
\input{Recdef/document/Nested1.tex}
\input{Recdef/document/Nested2.tex}
-\subsection{Partial functions}
+\subsection{Partial Functions}
\index{partial function}
\input{Advanced/document/Partial.tex}
\index{*recdef|)}
-\section{Advanced induction techniques}
+\section{Advanced Induction Techniques}
\label{sec:advanced-ind}
\index{induction|(}
\input{Misc/document/AdvancedInd.tex}