--- 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}
--- a/doc-src/TutorialI/Advanced/document/simp.tex Mon Mar 19 13:28:06 2001 +0100
+++ b/doc-src/TutorialI/Advanced/document/simp.tex Mon Mar 19 17:25:42 2001 +0100
@@ -125,7 +125,7 @@
such tricks.%
\end{isamarkuptext}%
%
-\isamarkupsubsection{How It Works%
+\isamarkupsubsection{How it Works%
}
%
\begin{isamarkuptext}%
--- a/doc-src/TutorialI/Advanced/simp.thy Mon Mar 19 13:28:06 2001 +0100
+++ b/doc-src/TutorialI/Advanced/simp.thy Mon Mar 19 17:25:42 2001 +0100
@@ -110,7 +110,7 @@
such tricks.
*}
-subsection{*How It Works*}
+subsection{*How it Works*}
text{*\label{sec:SimpHow}
Roughly speaking, the simplifier proceeds bottom-up (subterms are simplified
--- a/doc-src/TutorialI/Inductive/advanced-examples.tex Mon Mar 19 13:28:06 2001 +0100
+++ b/doc-src/TutorialI/Inductive/advanced-examples.tex Mon Mar 19 17:25:42 2001 +0100
@@ -114,7 +114,7 @@
\isa{set} of arguments expresses that all of them are well-formed.
-\subsection{Alternative Definition Using a monotone Function}
+\subsection{Alternative Definition Using a Monotone Function}
An inductive definition may refer to the inductively defined
set through an arbitrary monotone function. To demonstrate this
--- a/doc-src/TutorialI/Inductive/inductive.tex Mon Mar 19 13:28:06 2001 +0100
+++ b/doc-src/TutorialI/Inductive/inductive.tex Mon Mar 19 17:25:42 2001 +0100
@@ -18,7 +18,7 @@
\input{Inductive/document/Mutual}
\input{Inductive/document/Star}
-\section{Advanced inductive definitions}
+\section{Advanced Inductive Definitions}
\label{sec:adv-ind-def}
\input{Inductive/advanced-examples}
--- a/doc-src/TutorialI/Misc/document/natsum.tex Mon Mar 19 13:28:06 2001 +0100
+++ b/doc-src/TutorialI/Misc/document/natsum.tex Mon Mar 19 17:25:42 2001 +0100
@@ -61,7 +61,7 @@
\end{warn}
Simple arithmetic goals are proved automatically by both \isa{auto} and the
-simplification methods introduced in \S\ref{sec:Simplification}. For
+simplification method introduced in \S\ref{sec:Simplification}. For
example,%
\end{isamarkuptext}%
\isacommand{lemma}\ {\isachardoublequote}{\isasymlbrakk}\ {\isasymnot}\ m\ {\isacharless}\ n{\isacharsemicolon}\ m\ {\isacharless}\ n{\isacharplus}{\isadigit{1}}\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ m\ {\isacharequal}\ n{\isachardoublequote}%
--- a/doc-src/TutorialI/ToyList/ToyList.thy Mon Mar 19 13:28:06 2001 +0100
+++ b/doc-src/TutorialI/ToyList/ToyList.thy Mon Mar 19 17:25:42 2001 +0100
@@ -117,7 +117,7 @@
illustrate not just the basic proof commands but also the typical proof
process.
-\subsubsection*{Main goal: @{text"rev(rev xs) = xs"}.}
+\subsubsection*{Main Goal: @{text"rev(rev xs) = xs"}.}
Our goal is to show that reversing a list twice produces the original
list. The input line
--- a/doc-src/TutorialI/ToyList/document/ToyList.tex Mon Mar 19 13:28:06 2001 +0100
+++ b/doc-src/TutorialI/ToyList/document/ToyList.tex Mon Mar 19 17:25:42 2001 +0100
@@ -114,7 +114,7 @@
illustrate not just the basic proof commands but also the typical proof
process.
-\subsubsection*{Main goal: \isa{rev{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ xs}.}
+\subsubsection*{Main Goal: \isa{rev{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ xs}.}
Our goal is to show that reversing a list twice produces the original
list. The input line%
--- a/doc-src/TutorialI/Types/numerics.tex Mon Mar 19 13:28:06 2001 +0100
+++ b/doc-src/TutorialI/Types/numerics.tex Mon Mar 19 17:25:42 2001 +0100
@@ -87,7 +87,7 @@
-\subsection{The type of natural numbers, {\tt\slshape nat}}
+\subsection{The Type of Natural Numbers, {\tt\slshape nat}}
This type requires no introduction: we have been using it from the
beginning. Hundreds of theorems about the natural numbers are
@@ -198,7 +198,7 @@
\rulename{dvd_add}
\end{isabelle}
-\subsubsection{Simplifier tricks}
+\subsubsection{Simplifier Tricks}
The rule \isa{diff_mult_distrib} shown above is one of the few facts
about \isa{m\ -\ n} that is not subject to
the condition \isa{n\ \isasymle \ m}. Natural number subtraction has few
@@ -251,7 +251,7 @@
\end{isabelle}
-\subsection{The type of integers, {\tt\slshape int}}
+\subsection{The Type of Integers, {\tt\slshape int}}
Reasoning methods resemble those for the natural numbers, but induction and
the constant \isa{Suc} are not available. HOL provides many lemmas
@@ -333,7 +333,7 @@
\isa{zdiv_zmult2_eq} is $-2$ while the right-hand side is~$-1$.
-\subsection{The type of real numbers, {\tt\slshape real}}
+\subsection{The Type of Real Numbers, {\tt\slshape real}}
The real numbers enjoy two significant properties that the integers lack.
They are
--- a/doc-src/TutorialI/readers Mon Mar 19 13:28:06 2001 +0100
+++ b/doc-src/TutorialI/readers Mon Mar 19 17:25:42 2001 +0100
@@ -1,4 +1,5 @@
By chapter:
-Inductive definitions: Gerwin Klein
chapters 1 and 2, maybe 3: Peter White
+chapters 6, 7 and 8: David von Oheim
+chapter 6, maybe 8: Gerwin Klein