cite isabelle-axclass;
authorwenzelm
Sun, 21 May 2000 14:44:01 +0200
changeset 8901 e591fc327675
parent 8900 e9f1cd37cba4
child 8902 a705822f4e2a
cite isabelle-axclass;
doc-src/IsarRef/generic.tex
--- a/doc-src/IsarRef/generic.tex	Sun May 21 14:42:35 2000 +0200
+++ b/doc-src/IsarRef/generic.tex	Sun May 21 14:44:01 2000 +0200
@@ -13,10 +13,9 @@
 Axiomatic type classes are provided by Isabelle/Pure as a \emph{definitional}
 interface to type classes (cf.~\S\ref{sec:classes}).  Thus any object logic
 may make use of this light-weight mechanism of abstract theories
-\cite{Wenzel:1997:TPHOL}.  There is also a tutorial on \emph{Using Axiomatic
-  Type Classes in Isabelle} that is part of the standard Isabelle
-documentation.
-%FIXME cite
+\cite{Wenzel:1997:TPHOL}.  There is also a tutorial on using axiomatic type
+classes in isabelle \cite{isabelle-axclass} that is part of the standard
+Isabelle documentation.
 
 \begin{rail}
   'axclass' classdecl (axmdecl prop comment? +)