--- a/doc-src/IsarRef/generic.tex Thu Mar 07 12:03:43 2002 +0100
+++ b/doc-src/IsarRef/generic.tex Thu Mar 07 19:04:00 2002 +0100
@@ -37,8 +37,8 @@
of this class.
The ``axioms'' are stored as theorems according to the given name
- specifications, adding the class name $c$ as name space prefix; these facts
- are stored collectively as $c{\dtt}axioms$, too.
+ specifications, adding the class name $c$ as name space prefix; the same
+ facts are also stored collectively as $c{\dtt}axioms$.
\item [$\INSTANCE~c@1 \subseteq c@2$ and $\INSTANCE~t :: (\vec s)c$] setup a
goal stating a class relation or type arity. The proof would usually