# HG changeset patch
# User nipkow
# Date 985019142 -3600
# Node ID 279004936bb0c31301f4a54ad5c1e2623198bf0f
# Parent  b44ad7e4c4d26c9b208ff376d91e3c9e8bd3ca6c
*** empty log message ***

diff -r b44ad7e4c4d2 -r 279004936bb0 doc-src/TutorialI/Advanced/advanced.tex
--- 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}
diff -r b44ad7e4c4d2 -r 279004936bb0 doc-src/TutorialI/Advanced/document/simp.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}%
diff -r b44ad7e4c4d2 -r 279004936bb0 doc-src/TutorialI/Advanced/simp.thy
--- 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
diff -r b44ad7e4c4d2 -r 279004936bb0 doc-src/TutorialI/Inductive/advanced-examples.tex
--- 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
diff -r b44ad7e4c4d2 -r 279004936bb0 doc-src/TutorialI/Inductive/inductive.tex
--- 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}
 
diff -r b44ad7e4c4d2 -r 279004936bb0 doc-src/TutorialI/Misc/document/natsum.tex
--- 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}%
diff -r b44ad7e4c4d2 -r 279004936bb0 doc-src/TutorialI/ToyList/ToyList.thy
--- 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
diff -r b44ad7e4c4d2 -r 279004936bb0 doc-src/TutorialI/ToyList/document/ToyList.tex
--- 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%
diff -r b44ad7e4c4d2 -r 279004936bb0 doc-src/TutorialI/Types/numerics.tex
--- 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
diff -r b44ad7e4c4d2 -r 279004936bb0 doc-src/TutorialI/readers
--- 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