--- a/doc-src/IsarRef/generic.tex Tue Sep 06 16:29:39 2005 +0200
+++ b/doc-src/IsarRef/generic.tex Tue Sep 06 16:59:48 2005 +0200
@@ -27,18 +27,18 @@
\end{rail}
\begin{descr}
-
+
\item [$\AXCLASS~c \subseteq \vec c~~axms$] defines an axiomatic type class as
the intersection of existing classes, with additional axioms holding. Class
axioms may not contain more than one type variable. The class axioms (with
implicit sort constraints added) are bound to the given names. Furthermore
- a class introduction rule is generated (being bound as $c{.}intro$); this
- rule is employed by method $intro_classes$ to support instantiation proofs
- of this class.
-
+ a class introduction rule is generated (being bound as
+ $c_class{\dtt}intro$); this rule is employed by method $intro_classes$ to
+ support instantiation proofs of this class.
+
The ``axioms'' are stored as theorems according to the given name
specifications, adding the class name $c$ as name space prefix; the same
- facts are also stored collectively as $c{\dtt}axioms$.
+ facts are also stored collectively as $c_class{\dtt}axioms$.
\item [$\INSTANCE~c@1 \subseteq c@2$ and $\INSTANCE~t :: (\vec s)s$] setup a
goal stating a class relation or type arity. The proof would usually