diff -r 90583d625648 -r 021728c71030 doc-src/AxClass/axclass.tex
--- 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.