diff -r fc7841f31388 -r 813fabceec00 doc-src/AxClass/generated/NatClass.tex
--- a/doc-src/AxClass/generated/NatClass.tex	Mon May 22 10:31:44 2000 +0200
+++ b/doc-src/AxClass/generated/NatClass.tex	Mon May 22 11:56:55 2000 +0200
@@ -31,26 +31,28 @@
 \begin{isamarkuptext}%
 This is an abstract version of the plain $Nat$ theory in
  FOL.\footnote{See
- \url{http://isabelle.in.tum.de/library/FOL/ex/Nat.html}}
+ \url{http://isabelle.in.tum.de/library/FOL/ex/Nat.html}} Basically,
+ we have just replaced all occurrences of type $nat$ by $\alpha$ and
+ used the natural number axioms to define class $nat$.  There is only
+ a minor snag, that the original recursion operator $rec$ had to be
+ made monomorphic.
 
- Basically, we have just replaced all occurrences of type $nat$ by
- $\alpha$ and used the natural number axioms to define class $nat$.
- There is only a minor snag, that the original recursion operator
- $rec$ had to be made monomorphic, in a sense.  Thus class $nat$
- contains exactly those types $\tau$ that are isomorphic to ``the''
- natural numbers (with signature $0$, $Suc$, $rec$).
+ Thus class $nat$ contains exactly those types $\tau$ that are
+ isomorphic to ``the'' natural numbers (with signature $0$, $Suc$,
+ $rec$).
 
  \medskip What we have done here can be also viewed as \emph{type
  specification}.  Of course, it still remains open if there is some
  type at all that meets the class axioms.  Now a very nice property of
- axiomatic type classes is, that abstract reasoning is always possible
+ axiomatic type classes is that abstract reasoning is always possible
  --- independent of satisfiability.  The meta-logic won't break, even
- if some classes (or general sorts) turns out to be empty
- (``inconsistent'') later.
+ if some classes (or general sorts) turns out to be empty later ---
+ ``inconsistent'' class definitions may be useless, but do not cause
+ any harm.
 
  Theorems of the abstract natural numbers may be derived in the same
  way as for the concrete version.  The original proof scripts may be
- used with some trivial changes only (mostly adding some type
+ re-used with some trivial changes only (mostly adding some type
  constraints).%
 \end{isamarkuptext}%
 \isacommand{end}\end{isabelle}%