--- a/doc-src/AxClass/axclass.tex Mon May 10 15:35:03 1999 +0200
+++ b/doc-src/AxClass/axclass.tex Mon May 10 16:35:22 1999 +0200
@@ -560,7 +560,7 @@
``names''.
-\subsection{Defining natural numbers in \FOL}
+\subsection{Defining natural numbers in FOL}
\label{sec:ex-natclass}
Axiomatic type classes abstract over exactly one type argument. Thus,
@@ -625,7 +625,7 @@
some trivial modifications of the original \TT{Nat.ML}.
-\section{The user interface of \Isa's axclass package}
+\section{The user interface of Isabelle's axclass package}
The actual axiomatic type class package of \Isa/\Pure\ mainly consists
of two new theory sections: \TT{axclass} and \TT{instance}. Some
@@ -634,7 +634,7 @@
completely.
-\subsection{The \TT{axclass} section}
+\subsection{The axclass section}
Within theory files, \TT{axclass} introduces an axiomatic type class
definition. Its concrete syntax is:
@@ -674,7 +674,7 @@
$\idt{axm}_1, \ldots, \idt{axm}_m$ appropriately.
-\subsection{The \TT{instance} section}
+\subsection{The instance section}
Section \TT{instance} proves class inclusions or type arities at the
logical level and then transfers these into the type signature.