# HG changeset patch
# User wenzelm
# Date 926347680 -7200
# Node ID eca6105b1eaf14ebfc777fdc0ecf962fba4fe21c
# Parent  e0914e542f002f683547c4d92624176648e3735b
axclass;

diff -r e0914e542f00 -r eca6105b1eaf doc-src/Ref/theories.tex
--- a/doc-src/Ref/theories.tex	Mon May 10 16:47:53 1999 +0200
+++ b/doc-src/Ref/theories.tex	Mon May 10 16:48:00 1999 +0200
@@ -137,13 +137,13 @@
 \item[$constdefs$] combines the declaration of constants and their
   definition.  The first $string$ is the type, the second the definition.
   
-\item[$axclass$] \index{*axclass section} defines an
-  \rmindex{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, which is automatically
-  employed by $instance$ to prove instantiations of this class.
+\item[$axclass$] \index{*axclass section} defines an \rmindex{axiomatic type
+    class} \cite{Wenzel:1997:TPHOL} 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, which is automatically employed by $instance$ to prove
+  instantiations of this class.
   
 \item[$instance$] \index{*instance section} proves class inclusions or
   type arities at the logical level and then transfers these to the