# HG changeset patch
# User nipkow
# Date 973506743 -3600
# Node ID 5ab08609e6c8c31fb7e060ebe60d772ad82296f9
# Parent  7ef3807457430a3ef9b1cb71a31b4b09afb37847
*** empty log message ***

diff -r 7ef380745743 -r 5ab08609e6c8 doc-src/TutorialI/Advanced/WFrec.thy
--- a/doc-src/TutorialI/Advanced/WFrec.thy	Sat Nov 04 18:54:22 2000 +0100
+++ b/doc-src/TutorialI/Advanced/WFrec.thy	Mon Nov 06 11:32:23 2000 +0100
@@ -21,32 +21,24 @@
 component decreases (as in the inner call in the third equation).
 
 In general, \isacommand{recdef} supports termination proofs based on
-arbitrary \emph{well-founded relations}, i.e.\ \emph{well-founded
+arbitrary well-founded relations as introduced in \S\ref{sec:Well-founded}.
+This is called \textbf{well-founded
 recursion}\indexbold{recursion!well-founded}\index{well-founded
-recursion|see{recursion, well-founded}}.  A relation $<$ is
-\bfindex{well-founded} if it has no infinite descending chain $\cdots <
-a@2 < a@1 < a@0$. Clearly, a function definition is total iff the set
-of all pairs $(r,l)$, where $l$ is the argument on the left-hand side
-of an equation and $r$ the argument of some recursive call on the
-corresponding right-hand side, induces a well-founded relation.  For a
-systematic account of termination proofs via well-founded relations
-see, for example, \cite{Baader-Nipkow}. The HOL library formalizes
-some of the theory of well-founded relations. For example
-@{prop"wf r"}\index{*wf|bold} means that relation @{term[show_types]"r::('a*'a)set"} is
-well-founded.
+recursion|see{recursion, well-founded}}. Clearly, a function definition is
+total iff the set of all pairs $(r,l)$, where $l$ is the argument on the
+left-hand side of an equation and $r$ the argument of some recursive call on
+the corresponding right-hand side, induces a well-founded relation.  For a
+systematic account of termination proofs via well-founded relations see, for
+example, \cite{Baader-Nipkow}.
 
-Each \isacommand{recdef} definition should be accompanied (after the
-name of the function) by a well-founded relation on the argument type
-of the function. For example, \isaindexbold{measure} is defined by
-@{prop[display]"measure(f::'a \<Rightarrow> nat) \<equiv> {(y,x). f y < f x}"}
-and it has been proved that @{term"measure f"} is always well-founded.
-
-In addition to @{term measure}, the library provides
-a number of further constructions for obtaining well-founded relations.
-Above we have already met @{text"<*lex*>"} of type
-@{typ[display,source]"('a \<times> 'a)set \<Rightarrow> ('b \<times> 'b)set \<Rightarrow> (('a \<times> 'b) \<times> ('a \<times> 'b))set"}
-Of course the lexicographic product can also be interated, as in the following
-function definition:
+Each \isacommand{recdef} definition should be accompanied (after the name of
+the function) by a well-founded relation on the argument type of the
+function.  The HOL library formalizes some of the most important
+constructions of well-founded relations (see \S\ref{sec:Well-founded}). For
+example, @{term"measure f"} is always well-founded, and the lexicographic
+product of two well-founded relations is again well-founded, which we relied
+on when defining Ackermann's function above.
+Of course the lexicographic product can also be interated:
 *}
 
 consts contrived :: "nat \<times> nat \<times> nat \<Rightarrow> nat"
@@ -58,20 +50,10 @@
 "contrived(0,0,0)     = 0"
 
 text{*
-Lexicographic products of measure functions already go a long way. A
-further useful construction is the embedding of some type in an
-existing well-founded relation via the inverse image of a function:
-@{thm[display,show_types]inv_image_def[no_vars]}
-\begin{sloppypar}
-\noindent
-For example, @{term measure} is actually defined as @{term"inv_mage less_than"}, where
-@{term less_than} of type @{typ"(nat \<times> nat)set"} is the less-than relation on type @{typ nat}
-(as opposed to @{term"op <"}, which is of type @{typ"nat \<Rightarrow> nat \<Rightarrow> bool"}).
-\end{sloppypar}
-
-%Finally there is also {finite_psubset} the proper subset relation on finite sets
-
-All the above constructions are known to \isacommand{recdef}. Thus you
+Lexicographic products of measure functions already go a long
+way. Furthermore you may embedding some type in an
+existing well-founded relation via the inverse image construction @{term
+inv_image}. All these constructions are known to \isacommand{recdef}. Thus you
 will never have to prove well-foundedness of any relation composed
 solely of these building blocks. But of course the proof of
 termination of your function definition, i.e.\ that the arguments
@@ -87,18 +69,18 @@
 "f 0 = 0"
 "f (Suc n) = f n"
 
-text{*
+text{*\noindent
 Since \isacommand{recdef} is not prepared for @{term id}, the identity
 function, this leads to the complaint that it could not prove
-@{prop"wf (id less_than)"}, the well-foundedness of @{term"id
-less_than"}. We should first have proved that @{term id} preserves well-foundedness
+@{prop"wf (id less_than)"}.
+We should first have proved that @{term id} preserves well-foundedness
 *}
 
 lemma wf_id: "wf r \<Longrightarrow> wf(id r)"
 by simp;
 
 text{*\noindent
-and should have added the following hint to our above definition:
+and should have appended the following hint to our above definition:
 *}
 (*<*)
 consts g :: "nat \<Rightarrow> nat"
@@ -107,4 +89,4 @@
 "g (Suc n) = g n"
 (*>*)
 (hints recdef_wf add: wf_id)
-(*<*)end(*>*)
\ No newline at end of file
+(*<*)end(*>*)
diff -r 7ef380745743 -r 5ab08609e6c8 doc-src/TutorialI/Advanced/document/WFrec.tex
--- a/doc-src/TutorialI/Advanced/document/WFrec.tex	Sat Nov 04 18:54:22 2000 +0100
+++ b/doc-src/TutorialI/Advanced/document/WFrec.tex	Mon Nov 06 11:32:23 2000 +0100
@@ -23,36 +23,24 @@
 component decreases (as in the inner call in the third equation).
 
 In general, \isacommand{recdef} supports termination proofs based on
-arbitrary \emph{well-founded relations}, i.e.\ \emph{well-founded
+arbitrary well-founded relations as introduced in \S\ref{sec:Well-founded}.
+This is called \textbf{well-founded
 recursion}\indexbold{recursion!well-founded}\index{well-founded
-recursion|see{recursion, well-founded}}.  A relation $<$ is
-\bfindex{well-founded} if it has no infinite descending chain $\cdots <
-a@2 < a@1 < a@0$. Clearly, a function definition is total iff the set
-of all pairs $(r,l)$, where $l$ is the argument on the left-hand side
-of an equation and $r$ the argument of some recursive call on the
-corresponding right-hand side, induces a well-founded relation.  For a
-systematic account of termination proofs via well-founded relations
-see, for example, \cite{Baader-Nipkow}. The HOL library formalizes
-some of the theory of well-founded relations. For example
-\isa{wf\ r}\index{*wf|bold} means that relation \isa{r{\isasymColon}{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set} is
-well-founded.
+recursion|see{recursion, well-founded}}. Clearly, a function definition is
+total iff the set of all pairs $(r,l)$, where $l$ is the argument on the
+left-hand side of an equation and $r$ the argument of some recursive call on
+the corresponding right-hand side, induces a well-founded relation.  For a
+systematic account of termination proofs via well-founded relations see, for
+example, \cite{Baader-Nipkow}.
 
-Each \isacommand{recdef} definition should be accompanied (after the
-name of the function) by a well-founded relation on the argument type
-of the function. For example, \isaindexbold{measure} is defined by
-\begin{isabelle}%
-\ \ \ \ \ measure\ f\ {\isasymequiv}\ {\isacharbraceleft}{\isacharparenleft}y{\isacharcomma}\ x{\isacharparenright}{\isachardot}\ f\ y\ {\isacharless}\ f\ x{\isacharbraceright}%
-\end{isabelle}
-and it has been proved that \isa{measure\ f} is always well-founded.
-
-In addition to \isa{measure}, the library provides
-a number of further constructions for obtaining well-founded relations.
-Above we have already met \isa{{\isacharless}{\isacharasterisk}lex{\isacharasterisk}{\isachargreater}} of type
-\begin{isabelle}%
-\ \ \ \ \ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}b\ {\isasymtimes}\ {\isacharprime}b{\isacharparenright}set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b{\isacharparenright}\ {\isasymtimes}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b{\isacharparenright}{\isacharparenright}set{\isachardoublequote}%
-\end{isabelle}
-Of course the lexicographic product can also be interated, as in the following
-function definition:%
+Each \isacommand{recdef} definition should be accompanied (after the name of
+the function) by a well-founded relation on the argument type of the
+function.  The HOL library formalizes some of the most important
+constructions of well-founded relations (see \S\ref{sec:Well-founded}). For
+example, \isa{measure\ f} is always well-founded, and the lexicographic
+product of two well-founded relations is again well-founded, which we relied
+on when defining Ackermann's function above.
+Of course the lexicographic product can also be interated:%
 \end{isamarkuptext}%
 \isacommand{consts}\ contrived\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ {\isasymtimes}\ nat\ {\isasymtimes}\ nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline
 \isacommand{recdef}\ contrived\isanewline
@@ -62,23 +50,9 @@
 {\isachardoublequote}contrived{\isacharparenleft}Suc\ i{\isacharcomma}{\isadigit{0}}{\isacharcomma}{\isadigit{0}}{\isacharparenright}\ {\isacharequal}\ contrived{\isacharparenleft}i{\isacharcomma}i{\isacharcomma}i{\isacharparenright}{\isachardoublequote}\isanewline
 {\isachardoublequote}contrived{\isacharparenleft}{\isadigit{0}}{\isacharcomma}{\isadigit{0}}{\isacharcomma}{\isadigit{0}}{\isacharparenright}\ \ \ \ \ {\isacharequal}\ {\isadigit{0}}{\isachardoublequote}%
 \begin{isamarkuptext}%
-Lexicographic products of measure functions already go a long way. A
-further useful construction is the embedding of some type in an
-existing well-founded relation via the inverse image of a function:
-\begin{isabelle}%
-\ \ \ \ \ inv{\isacharunderscore}image\ {\isacharparenleft}r{\isasymColon}{\isacharparenleft}{\isacharprime}b\ {\isasymtimes}\ {\isacharprime}b{\isacharparenright}\ set{\isacharparenright}\ {\isacharparenleft}f{\isasymColon}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b{\isacharparenright}\ {\isasymequiv}\isanewline
-\ \ \ \ \ {\isacharbraceleft}{\isacharparenleft}x{\isasymColon}{\isacharprime}a{\isacharcomma}\ y{\isasymColon}{\isacharprime}a{\isacharparenright}{\isachardot}\ {\isacharparenleft}f\ x{\isacharcomma}\ f\ y{\isacharparenright}\ {\isasymin}\ r{\isacharbraceright}%
-\end{isabelle}
-\begin{sloppypar}
-\noindent
-For example, \isa{measure} is actually defined as \isa{inv{\isacharunderscore}mage\ less{\isacharunderscore}than}, where
-\isa{less{\isacharunderscore}than} of type \isa{{\isacharparenleft}nat\ {\isasymtimes}\ nat{\isacharparenright}\ set} is the less-than relation on type \isa{nat}
-(as opposed to \isa{op\ {\isacharless}}, which is of type \isa{{\isacharbrackleft}nat{\isacharcomma}\ nat{\isacharbrackright}\ {\isasymRightarrow}\ bool}).
-\end{sloppypar}
-
-%Finally there is also {finite_psubset} the proper subset relation on finite sets
-
-All the above constructions are known to \isacommand{recdef}. Thus you
+Lexicographic products of measure functions already go a long
+way. Furthermore you may embedding some type in an
+existing well-founded relation via the inverse image construction \isa{inv{\isacharunderscore}image}. All these constructions are known to \isacommand{recdef}. Thus you
 will never have to prove well-foundedness of any relation composed
 solely of these building blocks. But of course the proof of
 termination of your function definition, i.e.\ that the arguments
@@ -93,15 +67,17 @@
 {\isachardoublequote}f\ {\isadigit{0}}\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequote}\isanewline
 {\isachardoublequote}f\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharequal}\ f\ n{\isachardoublequote}%
 \begin{isamarkuptext}%
+\noindent
 Since \isacommand{recdef} is not prepared for \isa{id}, the identity
 function, this leads to the complaint that it could not prove
-\isa{wf\ {\isacharparenleft}id\ less{\isacharunderscore}than{\isacharparenright}}, the well-foundedness of \isa{id\ less{\isacharunderscore}than}. We should first have proved that \isa{id} preserves well-foundedness%
+\isa{wf\ {\isacharparenleft}id\ less{\isacharunderscore}than{\isacharparenright}}.
+We should first have proved that \isa{id} preserves well-foundedness%
 \end{isamarkuptext}%
 \isacommand{lemma}\ wf{\isacharunderscore}id{\isacharcolon}\ {\isachardoublequote}wf\ r\ {\isasymLongrightarrow}\ wf{\isacharparenleft}id\ r{\isacharparenright}{\isachardoublequote}\isanewline
 \isacommand{by}\ simp%
 \begin{isamarkuptext}%
 \noindent
-and should have added the following hint to our above definition:%
+and should have appended the following hint to our above definition:%
 \end{isamarkuptext}%
 {\isacharparenleft}\isakeyword{hints}\ recdef{\isacharunderscore}wf\ add{\isacharcolon}\ wf{\isacharunderscore}id{\isacharparenright}\end{isabellebody}%
 %%% Local Variables:
diff -r 7ef380745743 -r 5ab08609e6c8 doc-src/TutorialI/Inductive/AB.thy
--- a/doc-src/TutorialI/Inductive/AB.thy	Sat Nov 04 18:54:22 2000 +0100
+++ b/doc-src/TutorialI/Inductive/AB.thy	Mon Nov 06 11:32:23 2000 +0100
@@ -303,6 +303,6 @@
 similar to the other cases (which are automatic in Isabelle). We conclude
 that the authors are at least cavalier about this point and may even have
 overlooked the slight difficulty lurking in the omitted cases. This is not
-atypical for pen-and-paper proofs, once analysed in detail.  *}
+atypical for pencil-and-paper proofs, once analysed in detail.  *}
 
 (*<*)end(*>*)
diff -r 7ef380745743 -r 5ab08609e6c8 doc-src/TutorialI/Inductive/Star.thy
--- a/doc-src/TutorialI/Inductive/Star.thy	Sat Nov 04 18:54:22 2000 +0100
+++ b/doc-src/TutorialI/Inductive/Star.thy	Mon Nov 06 11:32:23 2000 +0100
@@ -8,10 +8,9 @@
 
 A perfect example of an inductive definition is the reflexive transitive
 closure of a relation. This concept was already introduced in
-\S\ref{sec:rtrancl}, but it was not shown how it is defined. In fact,
-the operator @{text"^*"} is not defined inductively but via a least
-fixed point because at that point in the theory hierarchy
-inductive definitions are not yet available. But now they are:
+\S\ref{sec:Relations}, where the operator @{text"^*"} was
+defined as a least fixed point because
+inductive definitions were not yet available. But now they are:
 *}
 
 consts rtc :: "('a \<times> 'a)set \<Rightarrow> ('a \<times> 'a)set"   ("_*" [1000] 999)
diff -r 7ef380745743 -r 5ab08609e6c8 doc-src/TutorialI/Inductive/document/AB.tex
--- a/doc-src/TutorialI/Inductive/document/AB.tex	Sat Nov 04 18:54:22 2000 +0100
+++ b/doc-src/TutorialI/Inductive/document/AB.tex	Mon Nov 06 11:32:23 2000 +0100
@@ -276,7 +276,7 @@
 similar to the other cases (which are automatic in Isabelle). We conclude
 that the authors are at least cavalier about this point and may even have
 overlooked the slight difficulty lurking in the omitted cases. This is not
-atypical for pen-and-paper proofs, once analysed in detail.%
+atypical for pencil-and-paper proofs, once analysed in detail.%
 \end{isamarkuptext}%
 \end{isabellebody}%
 %%% Local Variables:
diff -r 7ef380745743 -r 5ab08609e6c8 doc-src/TutorialI/Inductive/document/Star.tex
--- a/doc-src/TutorialI/Inductive/document/Star.tex	Sat Nov 04 18:54:22 2000 +0100
+++ b/doc-src/TutorialI/Inductive/document/Star.tex	Mon Nov 06 11:32:23 2000 +0100
@@ -12,10 +12,9 @@
 
 A perfect example of an inductive definition is the reflexive transitive
 closure of a relation. This concept was already introduced in
-\S\ref{sec:rtrancl}, but it was not shown how it is defined. In fact,
-the operator \isa{{\isacharcircum}{\isacharasterisk}} is not defined inductively but via a least
-fixed point because at that point in the theory hierarchy
-inductive definitions are not yet available. But now they are:%
+\S\ref{sec:Relations}, where the operator \isa{{\isacharcircum}{\isacharasterisk}} was
+defined as a least fixed point because
+inductive definitions were not yet available. But now they are:%
 \end{isamarkuptext}%
 \isacommand{consts}\ rtc\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}set{\isachardoublequote}\ \ \ {\isacharparenleft}{\isachardoublequote}{\isacharunderscore}{\isacharasterisk}{\isachardoublequote}\ {\isacharbrackleft}{\isadigit{1}}{\isadigit{0}}{\isadigit{0}}{\isadigit{0}}{\isacharbrackright}\ {\isadigit{9}}{\isadigit{9}}{\isadigit{9}}{\isacharparenright}\isanewline
 \isacommand{inductive}\ {\isachardoublequote}r{\isacharasterisk}{\isachardoublequote}\isanewline
diff -r 7ef380745743 -r 5ab08609e6c8 doc-src/TutorialI/Misc/AdvancedInd.thy
--- a/doc-src/TutorialI/Misc/AdvancedInd.thy	Sat Nov 04 18:54:22 2000 +0100
+++ b/doc-src/TutorialI/Misc/AdvancedInd.thy	Mon Nov 06 11:32:23 2000 +0100
@@ -5,9 +5,10 @@
 text{*\noindent
 Now that we have learned about rules and logic, we take another look at the
 finer points of induction. The two questions we answer are: what to do if the
-proposition to be proved is not directly amenable to induction, and how to
-utilize and even derive new induction schemas. We conclude with some slightly subtle
-examples of induction.
+proposition to be proved is not directly amenable to induction
+(\S\ref{sec:ind-var-in-prems}), and how to utilize (\S\ref{sec:complete-ind})
+and even derive (\S\ref{sec:derive-ind}) new induction schemas. We conclude
+with an extended example of induction (\S\ref{sec:CTL-revisited}).
 *};
 
 subsection{*Massaging the proposition*};
@@ -160,7 +161,7 @@
 not introduce an inconsistency because, for example, the identity function
 satisfies it.}
 for @{term"f"} it follows that @{prop"n <= f n"}, which can
-be proved by induction on @{term"f n"}. Following the recipy outlined
+be proved by induction on @{term"f n"}. Following the recipe outlined
 above, we have to phrase the proposition as follows to allow induction:
 *};
 
@@ -278,7 +279,7 @@
 Now it is straightforward to derive the original version of
 @{thm[source]nat_less_induct} by manipulting the conclusion of the above lemma:
 instantiate @{term"n"} by @{term"Suc n"} and @{term"m"} by @{term"n"} and
-remove the trivial condition @{prop"n < Sc n"}. Fortunately, this
+remove the trivial condition @{prop"n < Suc n"}. Fortunately, this
 happens automatically when we add the lemma as a new premise to the
 desired goal:
 *};
@@ -287,17 +288,11 @@
 by(insert induct_lem, blast);
 
 text{*
-Finally we should mention that HOL already provides the mother of all
-inductions, \textbf{well-founded
-induction}\indexbold{induction!well-founded}\index{well-founded
-induction|see{induction, well-founded}} (@{thm[source]wf_induct}):
-@{thm[display]wf_induct[no_vars]}
-where @{term"wf r"} means that the relation @{term r} is well-founded
-(see \S\ref{sec:well-founded}).
-For example, theorem @{thm[source]nat_less_induct} can be viewed (and
-derived) as a special case of @{thm[source]wf_induct} where 
-@{term r} is @{text"<"} on @{typ nat}. The details can be found in the HOL library.
-For a mathematical account of well-founded induction see, for example, \cite{Baader-Nipkow}.
+Finally we should remind the reader that HOL already provides the mother of
+all inductions, well-founded induction (see \S\ref{sec:Well-founded}).  For
+example theorem @{thm[source]nat_less_induct} can be viewed (and derived) as
+a special case of @{thm[source]wf_induct} where @{term r} is @{text"<"} on
+@{typ nat}. The details can be found in the HOL library.
 *};
 
 (*<*)
diff -r 7ef380745743 -r 5ab08609e6c8 doc-src/TutorialI/Misc/document/AdvancedInd.tex
--- a/doc-src/TutorialI/Misc/document/AdvancedInd.tex	Sat Nov 04 18:54:22 2000 +0100
+++ b/doc-src/TutorialI/Misc/document/AdvancedInd.tex	Mon Nov 06 11:32:23 2000 +0100
@@ -6,13 +6,13 @@
 \noindent
 Now that we have learned about rules and logic, we take another look at the
 finer points of induction. The two questions we answer are: what to do if the
-proposition to be proved is not directly amenable to induction, and how to
-utilize and even derive new induction schemas. We conclude with some slightly subtle
-examples of induction.%
+proposition to be proved is not directly amenable to induction
+(\S\ref{sec:ind-var-in-prems}), and how to utilize (\S\ref{sec:complete-ind})
+and even derive (\S\ref{sec:derive-ind}) new induction schemas. We conclude
+with an extended example of induction (\S\ref{sec:CTL-revisited}).%
 \end{isamarkuptext}%
 %
-\isamarkupsubsection{Massaging the proposition%
-}
+\isamarkupsubsection{Massaging the proposition}
 %
 \begin{isamarkuptext}%
 \label{sec:ind-var-in-prems}
@@ -123,8 +123,7 @@
 the conclusion as well, under the \isa{{\isasymforall}}, again using \isa{{\isasymlongrightarrow}} as shown above.%
 \end{isamarkuptext}%
 %
-\isamarkupsubsection{Beyond structural and recursion induction%
-}
+\isamarkupsubsection{Beyond structural and recursion induction}
 %
 \begin{isamarkuptext}%
 \label{sec:complete-ind}
@@ -153,7 +152,7 @@
 not introduce an inconsistency because, for example, the identity function
 satisfies it.}
 for \isa{f} it follows that \isa{n\ {\isasymle}\ f\ n}, which can
-be proved by induction on \isa{f\ n}. Following the recipy outlined
+be proved by induction on \isa{f\ n}. Following the recipe outlined
 above, we have to phrase the proposition as follows to allow induction:%
 \end{isamarkuptext}%
 \isacommand{lemma}\ f{\isacharunderscore}incr{\isacharunderscore}lem{\isacharcolon}\ {\isachardoublequote}{\isasymforall}i{\isachardot}\ k\ {\isacharequal}\ f\ i\ {\isasymlongrightarrow}\ i\ {\isasymle}\ f\ i{\isachardoublequote}%
@@ -242,8 +241,7 @@
 \end{quote}%
 \end{isamarkuptext}%
 %
-\isamarkupsubsection{Derivation of new induction schemas%
-}
+\isamarkupsubsection{Derivation of new induction schemas}
 %
 \begin{isamarkuptext}%
 \label{sec:derive-ind}
@@ -273,26 +271,18 @@
 Now it is straightforward to derive the original version of
 \isa{nat{\isacharunderscore}less{\isacharunderscore}induct} by manipulting the conclusion of the above lemma:
 instantiate \isa{n} by \isa{Suc\ n} and \isa{m} by \isa{n} and
-remove the trivial condition \isa{n\ {\isacharless}\ Sc\ n}. Fortunately, this
+remove the trivial condition \isa{n\ {\isacharless}\ Suc\ n}. Fortunately, this
 happens automatically when we add the lemma as a new premise to the
 desired goal:%
 \end{isamarkuptext}%
 \isacommand{theorem}\ nat{\isacharunderscore}less{\isacharunderscore}induct{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isasymAnd}n{\isacharcolon}{\isacharcolon}nat{\isachardot}\ {\isasymforall}m{\isacharless}n{\isachardot}\ P\ m\ {\isasymLongrightarrow}\ P\ n{\isacharparenright}\ {\isasymLongrightarrow}\ P\ n{\isachardoublequote}\isanewline
 \isacommand{by}{\isacharparenleft}insert\ induct{\isacharunderscore}lem{\isacharcomma}\ blast{\isacharparenright}%
 \begin{isamarkuptext}%
-Finally we should mention that HOL already provides the mother of all
-inductions, \textbf{well-founded
-induction}\indexbold{induction!well-founded}\index{well-founded
-induction|see{induction, well-founded}} (\isa{wf{\isacharunderscore}induct}):
-\begin{isabelle}%
-\ \ \ \ \ {\isasymlbrakk}wf\ r{\isacharsemicolon}\ {\isasymAnd}x{\isachardot}\ {\isasymforall}y{\isachardot}\ {\isacharparenleft}y{\isacharcomma}\ x{\isacharparenright}\ {\isasymin}\ r\ {\isasymlongrightarrow}\ P\ y\ {\isasymLongrightarrow}\ P\ x{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ a%
-\end{isabelle}
-where \isa{wf\ r} means that the relation \isa{r} is well-founded
-(see \S\ref{sec:well-founded}).
-For example, theorem \isa{nat{\isacharunderscore}less{\isacharunderscore}induct} can be viewed (and
-derived) as a special case of \isa{wf{\isacharunderscore}induct} where 
-\isa{r} is \isa{{\isacharless}} on \isa{nat}. The details can be found in the HOL library.
-For a mathematical account of well-founded induction see, for example, \cite{Baader-Nipkow}.%
+Finally we should remind the reader that HOL already provides the mother of
+all inductions, well-founded induction (see \S\ref{sec:Well-founded}).  For
+example theorem \isa{nat{\isacharunderscore}less{\isacharunderscore}induct} can be viewed (and derived) as
+a special case of \isa{wf{\isacharunderscore}induct} where \isa{r} is \isa{{\isacharless}} on
+\isa{nat}. The details can be found in the HOL library.%
 \end{isamarkuptext}%
 \end{isabellebody}%
 %%% Local Variables:
diff -r 7ef380745743 -r 5ab08609e6c8 doc-src/TutorialI/Misc/document/Itrev.tex
--- a/doc-src/TutorialI/Misc/document/Itrev.tex	Sat Nov 04 18:54:22 2000 +0100
+++ b/doc-src/TutorialI/Misc/document/Itrev.tex	Mon Nov 06 11:32:23 2000 +0100
@@ -2,8 +2,7 @@
 \begin{isabellebody}%
 \def\isabellecontext{Itrev}%
 %
-\isamarkupsection{Induction heuristics%
-}
+\isamarkupsection{Induction heuristics}
 %
 \begin{isamarkuptext}%
 \label{sec:InductionHeuristics}
diff -r 7ef380745743 -r 5ab08609e6c8 doc-src/TutorialI/Misc/document/case_exprs.tex
--- a/doc-src/TutorialI/Misc/document/case_exprs.tex	Sat Nov 04 18:54:22 2000 +0100
+++ b/doc-src/TutorialI/Misc/document/case_exprs.tex	Mon Nov 06 11:32:23 2000 +0100
@@ -2,8 +2,7 @@
 \begin{isabellebody}%
 \def\isabellecontext{case{\isacharunderscore}exprs}%
 %
-\isamarkupsubsection{Case expressions%
-}
+\isamarkupsubsection{Case expressions}
 %
 \begin{isamarkuptext}%
 \label{sec:case-expressions}
@@ -49,8 +48,7 @@
 indicate their scope%
 \end{isamarkuptext}%
 %
-\isamarkupsubsection{Structural induction and case distinction%
-}
+\isamarkupsubsection{Structural induction and case distinction}
 %
 \begin{isamarkuptext}%
 \indexbold{structural induction}
diff -r 7ef380745743 -r 5ab08609e6c8 doc-src/TutorialI/Misc/document/simp.tex
--- a/doc-src/TutorialI/Misc/document/simp.tex	Sat Nov 04 18:54:22 2000 +0100
+++ b/doc-src/TutorialI/Misc/document/simp.tex	Mon Nov 06 11:32:23 2000 +0100
@@ -2,8 +2,7 @@
 \begin{isabellebody}%
 \def\isabellecontext{simp}%
 %
-\isamarkupsubsubsection{Simplification rules%
-}
+\isamarkupsubsubsection{Simplification rules}
 %
 \begin{isamarkuptext}%
 \indexbold{simplification rule}
@@ -40,8 +39,7 @@
 \end{warn}%
 \end{isamarkuptext}%
 %
-\isamarkupsubsubsection{The simplification method%
-}
+\isamarkupsubsubsection{The simplification method}
 %
 \begin{isamarkuptext}%
 \index{*simp (method)|bold}
@@ -57,8 +55,7 @@
 Note that \isa{simp} fails if nothing changes.%
 \end{isamarkuptext}%
 %
-\isamarkupsubsubsection{Adding and deleting simplification rules%
-}
+\isamarkupsubsubsection{Adding and deleting simplification rules}
 %
 \begin{isamarkuptext}%
 If a certain theorem is merely needed in a few proofs by simplification,
@@ -76,8 +73,7 @@
 \end{quote}%
 \end{isamarkuptext}%
 %
-\isamarkupsubsubsection{Assumptions%
-}
+\isamarkupsubsubsection{Assumptions}
 %
 \begin{isamarkuptext}%
 \index{simplification!with/of assumptions}
@@ -127,8 +123,7 @@
 other arguments.%
 \end{isamarkuptext}%
 %
-\isamarkupsubsubsection{Rewriting with definitions%
-}
+\isamarkupsubsubsection{Rewriting with definitions}
 %
 \begin{isamarkuptext}%
 \index{simplification!with definitions}
@@ -176,8 +171,7 @@
 \end{warn}%
 \end{isamarkuptext}%
 %
-\isamarkupsubsubsection{Simplifying let-expressions%
-}
+\isamarkupsubsubsection{Simplifying let-expressions}
 %
 \begin{isamarkuptext}%
 \index{simplification!of let-expressions}
@@ -196,8 +190,7 @@
 default:%
 \end{isamarkuptext}%
 \isacommand{declare}\ Let{\isacharunderscore}def\ {\isacharbrackleft}simp{\isacharbrackright}%
-\isamarkupsubsubsection{Conditional equations%
-}
+\isamarkupsubsubsection{Conditional equations}
 %
 \begin{isamarkuptext}%
 So far all examples of rewrite rules were equations. The simplifier also
@@ -224,8 +217,7 @@
 assumption of the subgoal.%
 \end{isamarkuptext}%
 %
-\isamarkupsubsubsection{Automatic case splits%
-}
+\isamarkupsubsubsection{Automatic case splits}
 %
 \begin{isamarkuptext}%
 \indexbold{case splits}\index{*split|(}
@@ -318,8 +310,7 @@
 \index{*split|)}%
 \end{isamarkuptxt}%
 %
-\isamarkupsubsubsection{Arithmetic%
-}
+\isamarkupsubsubsection{Arithmetic}
 %
 \begin{isamarkuptext}%
 \index{arithmetic}
@@ -339,8 +330,7 @@
 is not proved by simplification and requires \isa{arith}.%
 \end{isamarkuptext}%
 %
-\isamarkupsubsubsection{Tracing%
-}
+\isamarkupsubsubsection{Tracing}
 %
 \begin{isamarkuptext}%
 \indexbold{tracing the simplifier}
diff -r 7ef380745743 -r 5ab08609e6c8 doc-src/TutorialI/Types/Axioms.thy
--- a/doc-src/TutorialI/Types/Axioms.thy	Sat Nov 04 18:54:22 2000 +0100
+++ b/doc-src/TutorialI/Types/Axioms.thy	Mon Nov 06 11:32:23 2000 +0100
@@ -135,30 +135,11 @@
  apply(blast intro: refl);
 done
 
-text{*\noindent
-The result is the following subclass diagram:
-\[
-\begin{array}{c}
-\isa{term}\\
-|\\
-\isa{ordrel}\\
-|\\
-\isa{strord}\\
-|\\
-\isa{parord}
-\end{array}
-\]
+text{*
+The subclass relation must always be acyclic. Therefore Isabelle will
+complain if you also prove the relationship @{text"strord < parord"}.
+*}
 
-In general, the subclass diagram must be acyclic. Therefore Isabelle will
-complain if you also prove the relationship @{text"strord < parord"}.
-Multiple inheritance is however permitted.
-
-This finishes our demonstration of type classes based on orderings.  We
-remind our readers that \isa{Main} contains a much more developed theory of
-orderings phrased in terms of the usual @{text"\<le>"} and @{text"<"}.
-It is recommended that, if possible,
-you base your own ordering relations on this theory.
-*}
 
 (*
 instance strord < parord
@@ -174,6 +155,61 @@
 done
 *)
 
+subsubsection{*Multiple inheritance and sorts*}
+
+text{*
+A class may inherit from more than one direct superclass. This is called
+multiple inheritance and is certainly permitted. For example we could define
+the classes of well-founded orderings and well-orderings:
+*}
+
+axclass wford < parord
+wford: "wf {(y,x). y << x}"
+
+axclass wellord < linord, wford
+
+text{*\noindent
+The last line expresses the usual definition: a well-ordering is a linear
+well-founded ordering. The result is the subclass diagram in
+Figure~\ref{fig:subclass}.
+
+\begin{figure}[htbp]
+\[
+\begin{array}{r@ {}r@ {}c@ {}l@ {}l}
+& & \isa{term}\\
+& & |\\
+& & \isa{ordrel}\\
+& & |\\
+& & \isa{strord}\\
+& & |\\
+& & \isa{parord} \\
+& / & & \backslash \\
+\isa{linord} & & & & \isa{wford} \\
+& \backslash & & / \\
+& & \isa{wellord}
+\end{array}
+\]
+\caption{Subclass diagramm}
+\label{fig:subclass}
+\end{figure}
+
+Since class @{text wellord} does not introduce any new axioms, it can simply
+be viewed as the intersection of the two classes @{text linord} and @{text
+wford}. Such intersections need not be given a new name but can be created on
+the fly: the expression $\{C@1,\dots,C@n\}$, where the $C@i$ are classes,
+represents the intersection of the $C@i$. Such an expression is called a
+\bfindex{sort}, and sorts can appear in most places where we have only shown
+classes so far, for example in type constraints: @{text"'a::{linord,wford}"}.
+In fact, @{text"'a::ord"} is short for @{text"'a::{ord}"}.
+However, we do not pursue this rarefied concept further.
+
+This concludes our demonstration of type classes based on orderings.  We
+remind our readers that \isa{Main} contains a theory of
+orderings phrased in terms of the usual @{text"\<le>"} and @{text"<"}.
+It is recommended that, if possible,
+you base your own ordering relations on this theory.
+*}
+
 subsubsection{*Inconsistencies*}
 
 text{* The reader may be wondering what happens if we, maybe accidentally,
diff -r 7ef380745743 -r 5ab08609e6c8 doc-src/TutorialI/Types/Overloading1.thy
--- a/doc-src/TutorialI/Types/Overloading1.thy	Sat Nov 04 18:54:22 2000 +0100
+++ b/doc-src/TutorialI/Types/Overloading1.thy	Mon Nov 06 11:32:23 2000 +0100
@@ -26,6 +26,10 @@
        le   :: "('a::ordrel) \<Rightarrow> 'a \<Rightarrow> bool"     (infixl "<<=" 50)
 
 text{*\noindent
+Note that only one occurrence of a type variable in a type needs to be
+constrained with a class; the constraint is propagated to the other
+occurrences automatically.
+
 So far there is not a single type of class @{text ordrel}. To breathe life
 into @{text ordrel} we need to declare a type to be an \bfindex{instance} of
 @{text ordrel}:
diff -r 7ef380745743 -r 5ab08609e6c8 doc-src/TutorialI/Types/Overloading2.thy
--- a/doc-src/TutorialI/Types/Overloading2.thy	Sat Nov 04 18:54:22 2000 +0100
+++ b/doc-src/TutorialI/Types/Overloading2.thy	Mon Nov 06 11:32:23 2000 +0100
@@ -16,6 +16,35 @@
 
 text{*\noindent
 The infix function @{text"!"} yields the nth element of a list.
-%However, we retract the componetwise comparison of lists and return
-%Note: only one definition because based on name.
+*}
+
+subsubsection{*Predefined overloading*}
+
+text{*
+HOL comes with a number of overloaded constants and corresponding classes.
+The most important ones are listed in Table~\ref{tab:overloading}. They are
+defined on all numeric types and somtimes on other types as well, for example
+@{text"-"}, @{text"\<le>"} and @{text"<"} on sets.
+
+\begin{table}[htbp]
+\begin{center}
+\begin{tabular}{lll}
+Constant & Type & Syntax \\
+\hline
+@{term 0} & @{text "'a::zero"} \\
+@{text"+"} & @{text "('a::plus) \<Rightarrow> 'a \<Rightarrow> 'a"} & (infixl 65) \\
+@{text"-"} & @{text "('a::minus) \<Rightarrow> 'a \<Rightarrow> 'a"} &  (infixl 65) \\
+@{text"*"} & @{text "('a::times) \<Rightarrow> 'a \<Rightarrow> 'a"} & (infixl 70) \\
+@{text"^"} & @{text "('a::power) \<Rightarrow> nat \<Rightarrow> 'a"} & (infixr 80) \\
+@{text"-"} & @{text "('a::minus) \<Rightarrow> 'a"} \\
+@{term abs} &  @{text "('a::minus) \<Rightarrow> 'a"} \\
+@{text"\<le>"} & @{text "('a::ord) \<Rightarrow> 'a \<Rightarrow> bool"} & (infixl 50) \\
+@{text"<"} & @{text "('a::ord) \<Rightarrow> 'a \<Rightarrow> bool"} & (infixl 50) \\
+@{term min} &  @{text "('a::ord) \<Rightarrow> 'a \<Rightarrow> 'a"} \\
+@{term max} &  @{text "('a::ord) \<Rightarrow> 'a \<Rightarrow> 'a"} \\
+\end{tabular}
+\caption{Overloaded constants in HOL}
+\label{tab:overloading}
+\end{center}
+\end{table}
 *}(*<*)end(*>*)
diff -r 7ef380745743 -r 5ab08609e6c8 doc-src/TutorialI/Types/document/Axioms.tex
--- a/doc-src/TutorialI/Types/document/Axioms.tex	Sat Nov 04 18:54:22 2000 +0100
+++ b/doc-src/TutorialI/Types/document/Axioms.tex	Mon Nov 06 11:32:23 2000 +0100
@@ -2,8 +2,7 @@
 \begin{isabellebody}%
 \def\isabellecontext{Axioms}%
 %
-\isamarkupsubsection{Axioms%
-}
+\isamarkupsubsection{Axioms}
 %
 \begin{isamarkuptext}%
 Now we want to attach axioms to our classes. Then we can reason on the
@@ -12,8 +11,7 @@
 our above ordering relations.%
 \end{isamarkuptext}%
 %
-\isamarkupsubsubsection{Partial orders%
-}
+\isamarkupsubsubsection{Partial orders}
 %
 \begin{isamarkuptext}%
 A \emph{partial order} is a subclass of \isa{ordrel}
@@ -88,8 +86,7 @@
 proof for each instance.%
 \end{isamarkuptext}%
 %
-\isamarkupsubsubsection{Linear orders%
-}
+\isamarkupsubsubsection{Linear orders}
 %
 \begin{isamarkuptext}%
 If any two elements of a partial order are comparable it is a
@@ -115,8 +112,7 @@
 section.%
 \end{isamarkuptext}%
 %
-\isamarkupsubsubsection{Strict orders%
-}
+\isamarkupsubsubsection{Strict orders}
 %
 \begin{isamarkuptext}%
 An alternative axiomatization of partial orders takes \isa{{\isacharless}{\isacharless}} rather than
@@ -139,33 +135,64 @@
 \ \isacommand{apply}{\isacharparenleft}blast\ intro{\isacharcolon}\ refl{\isacharparenright}\isanewline
 \isacommand{done}%
 \begin{isamarkuptext}%
+The subclass relation must always be acyclic. Therefore Isabelle will
+complain if you also prove the relationship \isa{strord\ {\isacharless}\ parord}.%
+\end{isamarkuptext}%
+%
+\isamarkupsubsubsection{Multiple inheritance and sorts}
+%
+\begin{isamarkuptext}%
+A class may inherit from more than one direct superclass. This is called
+multiple inheritance and is certainly permitted. For example we could define
+the classes of well-founded orderings and well-orderings:%
+\end{isamarkuptext}%
+\isacommand{axclass}\ wford\ {\isacharless}\ parord\isanewline
+wford{\isacharcolon}\ {\isachardoublequote}wf\ {\isacharbraceleft}{\isacharparenleft}y{\isacharcomma}x{\isacharparenright}{\isachardot}\ y\ {\isacharless}{\isacharless}\ x{\isacharbraceright}{\isachardoublequote}\isanewline
+\isanewline
+\isacommand{axclass}\ wellord\ {\isacharless}\ linord{\isacharcomma}\ wford%
+\begin{isamarkuptext}%
 \noindent
-The result is the following subclass diagram:
+The last line expresses the usual definition: a well-ordering is a linear
+well-founded ordering. The result is the subclass diagram in
+Figure~\ref{fig:subclass}.
+
+\begin{figure}[htbp]
 \[
-\begin{array}{c}
-\isa{term}\\
-|\\
-\isa{ordrel}\\
-|\\
-\isa{strord}\\
-|\\
-\isa{parord}
+\begin{array}{r@ {}r@ {}c@ {}l@ {}l}
+& & \isa{term}\\
+& & |\\
+& & \isa{ordrel}\\
+& & |\\
+& & \isa{strord}\\
+& & |\\
+& & \isa{parord} \\
+& / & & \backslash \\
+\isa{linord} & & & & \isa{wford} \\
+& \backslash & & / \\
+& & \isa{wellord}
 \end{array}
 \]
+\caption{Subclass diagramm}
+\label{fig:subclass}
+\end{figure}
 
-In general, the subclass diagram must be acyclic. Therefore Isabelle will
-complain if you also prove the relationship \isa{strord\ {\isacharless}\ parord}.
-Multiple inheritance is however permitted.
+Since class \isa{wellord} does not introduce any new axioms, it can simply
+be viewed as the intersection of the two classes \isa{linord} and \isa{wford}. Such intersections need not be given a new name but can be created on
+the fly: the expression $\{C@1,\dots,C@n\}$, where the $C@i$ are classes,
+represents the intersection of the $C@i$. Such an expression is called a
+\bfindex{sort}, and sorts can appear in most places where we have only shown
+classes so far, for example in type constraints: \isa{{\isacharprime}a{\isacharcolon}{\isacharcolon}{\isacharbraceleft}linord{\isacharcomma}wford{\isacharbraceright}}.
+In fact, \isa{{\isacharprime}a{\isacharcolon}{\isacharcolon}ord} is short for \isa{{\isacharprime}a{\isacharcolon}{\isacharcolon}{\isacharbraceleft}ord{\isacharbraceright}}.
+However, we do not pursue this rarefied concept further.
 
-This finishes our demonstration of type classes based on orderings.  We
-remind our readers that \isa{Main} contains a much more developed theory of
+This concludes our demonstration of type classes based on orderings.  We
+remind our readers that \isa{Main} contains a theory of
 orderings phrased in terms of the usual \isa{{\isasymle}} and \isa{{\isacharless}}.
 It is recommended that, if possible,
 you base your own ordering relations on this theory.%
 \end{isamarkuptext}%
 %
-\isamarkupsubsubsection{Inconsistencies%
-}
+\isamarkupsubsubsection{Inconsistencies}
 %
 \begin{isamarkuptext}%
 The reader may be wondering what happens if we, maybe accidentally,
diff -r 7ef380745743 -r 5ab08609e6c8 doc-src/TutorialI/Types/document/Overloading0.tex
--- a/doc-src/TutorialI/Types/document/Overloading0.tex	Sat Nov 04 18:54:22 2000 +0100
+++ b/doc-src/TutorialI/Types/document/Overloading0.tex	Mon Nov 06 11:32:23 2000 +0100
@@ -8,8 +8,7 @@
 constant may have multiple definitions at non-overlapping types.%
 \end{isamarkuptext}%
 %
-\isamarkupsubsubsection{An initial example%
-}
+\isamarkupsubsubsection{An initial example}
 %
 \begin{isamarkuptext}%
 If we want to introduce the notion of an \emph{inverse} for arbitrary types we
diff -r 7ef380745743 -r 5ab08609e6c8 doc-src/TutorialI/Types/document/Overloading1.tex
--- a/doc-src/TutorialI/Types/document/Overloading1.tex	Sat Nov 04 18:54:22 2000 +0100
+++ b/doc-src/TutorialI/Types/document/Overloading1.tex	Mon Nov 06 11:32:23 2000 +0100
@@ -2,8 +2,7 @@
 \begin{isabellebody}%
 \def\isabellecontext{Overloading{\isadigit{1}}}%
 %
-\isamarkupsubsubsection{Controlled overloading with type classes%
-}
+\isamarkupsubsubsection{Controlled overloading with type classes}
 %
 \begin{isamarkuptext}%
 We now start with the theory of ordering relations, which we want to phrase
@@ -26,6 +25,10 @@
 \ \ \ \ \ \ \ le\ \ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}ordrel{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bool{\isachardoublequote}\ \ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isacharless}{\isacharless}{\isacharequal}{\isachardoublequote}\ {\isadigit{5}}{\isadigit{0}}{\isacharparenright}%
 \begin{isamarkuptext}%
 \noindent
+Note that only one occurrence of a type variable in a type needs to be
+constrained with a class; the constraint is propagated to the other
+occurrences automatically.
+
 So far there is not a single type of class \isa{ordrel}. To breathe life
 into \isa{ordrel} we need to declare a type to be an \bfindex{instance} of
 \isa{ordrel}:%
diff -r 7ef380745743 -r 5ab08609e6c8 doc-src/TutorialI/Types/document/Overloading2.tex
--- a/doc-src/TutorialI/Types/document/Overloading2.tex	Sat Nov 04 18:54:22 2000 +0100
+++ b/doc-src/TutorialI/Types/document/Overloading2.tex	Mon Nov 06 11:32:23 2000 +0100
@@ -16,9 +16,38 @@
 \ \ \ \ \ \ \ \ \ \ \ \ \ \ size\ xs\ {\isacharequal}\ size\ ys\ {\isasymand}\ {\isacharparenleft}{\isasymforall}i{\isacharless}size\ xs{\isachardot}\ xs{\isacharbang}i\ {\isacharless}{\isacharless}{\isacharequal}\ ys{\isacharbang}i{\isacharparenright}{\isachardoublequote}%
 \begin{isamarkuptext}%
 \noindent
-The infix function \isa{{\isacharbang}} yields the nth element of a list.
-%However, we retract the componetwise comparison of lists and return
-%Note: only one definition because based on name.%
+The infix function \isa{{\isacharbang}} yields the nth element of a list.%
+\end{isamarkuptext}%
+%
+\isamarkupsubsubsection{Predefined overloading}
+%
+\begin{isamarkuptext}%
+HOL comes with a number of overloaded constants and corresponding classes.
+The most important ones are listed in Table~\ref{tab:overloading}. They are
+defined on all numeric types and somtimes on other types as well, for example
+\isa{{\isacharminus}}, \isa{{\isasymle}} and \isa{{\isacharless}} on sets.
+
+\begin{table}[htbp]
+\begin{center}
+\begin{tabular}{lll}
+Constant & Type & Syntax \\
+\hline
+\isa{{\isadigit{0}}} & \isa{{\isacharprime}a{\isacharcolon}{\isacharcolon}zero} \\
+\isa{{\isacharplus}} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}plus{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} & (infixl 65) \\
+\isa{{\isacharminus}} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}minus{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} &  (infixl 65) \\
+\isa{{\isacharasterisk}} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}times{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} & (infixl 70) \\
+\isa{{\isacharcircum}} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}power{\isacharparenright}\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ {\isacharprime}a} & (infixr 80) \\
+\isa{{\isacharminus}} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}minus{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a} \\
+\isa{abs} &  \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}minus{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a} \\
+\isa{{\isasymle}} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}ord{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bool} & (infixl 50) \\
+\isa{{\isacharless}} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}ord{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bool} & (infixl 50) \\
+\isa{min} &  \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}ord{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} \\
+\isa{max} &  \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}ord{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} \\
+\end{tabular}
+\caption{Overloaded constants in HOL}
+\label{tab:overloading}
+\end{center}
+\end{table}%
 \end{isamarkuptext}%
 \end{isabellebody}%
 %%% Local Variables:
diff -r 7ef380745743 -r 5ab08609e6c8 doc-src/TutorialI/Types/document/Typedef.tex
--- a/doc-src/TutorialI/Types/document/Typedef.tex	Sat Nov 04 18:54:22 2000 +0100
+++ b/doc-src/TutorialI/Types/document/Typedef.tex	Mon Nov 06 11:32:23 2000 +0100
@@ -2,8 +2,7 @@
 \begin{isabellebody}%
 \def\isabellecontext{Typedef}%
 %
-\isamarkupsection{Introducing new types%
-}
+\isamarkupsection{Introducing new types}
 %
 \begin{isamarkuptext}%
 \label{sec:adv-typedef}
@@ -19,8 +18,7 @@
 \end{warn}%
 \end{isamarkuptext}%
 %
-\isamarkupsubsection{Declaring new types%
-}
+\isamarkupsubsection{Declaring new types}
 %
 \begin{isamarkuptext}%
 \label{sec:typedecl}
@@ -57,8 +55,7 @@
 unnecessary: a one-element type called \isa{unit} is already defined in HOL.%
 \end{isamarkuptext}%
 %
-\isamarkupsubsection{Defining new types%
-}
+\isamarkupsubsection{Defining new types}
 %
 \begin{isamarkuptext}%
 \label{sec:typedef}
diff -r 7ef380745743 -r 5ab08609e6c8 doc-src/TutorialI/Types/types.tex
--- a/doc-src/TutorialI/Types/types.tex	Sat Nov 04 18:54:22 2000 +0100
+++ b/doc-src/TutorialI/Types/types.tex	Mon Nov 06 11:32:23 2000 +0100
@@ -14,6 +14,18 @@
   types ({\S}\ref{sec:axclass}).
 \end{itemize}
 
+\section{Basic types}
+
+\subsection{Numbers}
+\label{sec:numbers}
+
+\subsection{Pairs}
+\label{sec:products}
+% Check refs to this section to see what is expected of it.
+
+\subsection{Records}
+\label{sec:records}
+
 \input{Types/document/Typedef}
 
 \section{Axiomatic type classes}
diff -r 7ef380745743 -r 5ab08609e6c8 doc-src/TutorialI/basics.tex
--- a/doc-src/TutorialI/basics.tex	Sat Nov 04 18:54:22 2000 +0100
+++ b/doc-src/TutorialI/basics.tex	Mon Nov 06 11:32:23 2000 +0100
@@ -186,8 +186,8 @@
 \ttindexboldpos{::}{$Isalamtc} binds weakly and should therefore be enclosed
 in parentheses: \isa{x < y::nat} is ill-typed because it is interpreted as
 \isa{(x < y)::nat}. The main reason for type constraints are overloaded
-functions like \isa{+}, \isa{*} and \isa{<}. (See \S\ref{sec:TypeClasses} for
-a full discussion of overloading.)
+functions like \isa{+}, \isa{*} and \isa{<}. See \S\ref{sec:overloading} for
+a full discussion of overloading.
 
 \begin{warn}
 In general, HOL's concrete syntax tries to follow the conventions of
diff -r 7ef380745743 -r 5ab08609e6c8 doc-src/TutorialI/fp.tex
--- a/doc-src/TutorialI/fp.tex	Sat Nov 04 18:54:22 2000 +0100
+++ b/doc-src/TutorialI/fp.tex	Mon Nov 06 11:32:23 2000 +0100
@@ -257,7 +257,7 @@
   \indexboldpos{\isasymle}{$HOL2arithrel} and
   \ttindexboldpos{<}{$HOL2arithrel} are overloaded, i.e.\ they are available
   not just for natural numbers but at other types as well (see
-  \S\ref{sec:TypeClasses}). For example, given the goal \isa{x+0 = x}, there
+  \S\ref{sec:overloading}). For example, given the goal \isa{x+0 = x}, there
   is nothing to indicate that you are talking about natural numbers.  Hence
   Isabelle can only infer that \isa{x} is of some arbitrary type where
   \isa{0} and \isa{+} are declared. As a consequence, you will be unable to
@@ -305,7 +305,7 @@
 \index{arithmetic|)}
 
 
-\subsection{Products}
+\subsection{Pairs}
 \input{Misc/document/pairs.tex}
 
 %FIXME move stuff below into section on proofs about products?
@@ -315,16 +315,16 @@
   of a term may differ, which can affect proofs. If you want to avoid this
   complication, use \isa{fst} and \isa{snd}, i.e.\ write
   \isa{\isasymlambda{}p.~fst p + snd p} instead of
-  \isa{\isasymlambda(x,y).~x + y}.  See~\S\ref{proofs-about-products} for
+  \isa{\isasymlambda(x,y).~x + y}.  See~\S\ref{sec:products} for
   theorem proving with tuple patterns.
 \end{warn}
 
-Note that products, like natural numbers, are datatypes, which means
+Note that products, like type \isa{nat}, are datatypes, which means
 in particular that \isa{induct_tac} and \isa{case_tac} are applicable to
-products (see \S\ref{proofs-about-products}).
+products (see \S\ref{sec:products}).
 
 Instead of tuples with many components (where ``many'' is not much above 2),
-it is far preferable to use record types (see \S\ref{sec:records}).
+it is far preferable to use records (see \S\ref{sec:records}).
 
 \section{Definitions}
 \label{sec:Definitions}