# HG changeset patch
# User haftmann
# Date 1161356844 -7200
# Node ID 22ae82f77c5e8a49ef3e2cf6df7dc5cadb5d6e90
# Parent  d6742ff3b522a390769f6c9e07b66212cda0e28e
small refinements

diff -r d6742ff3b522 -r 22ae82f77c5e doc-src/IsarRef/generic.tex
--- a/doc-src/IsarRef/generic.tex	Fri Oct 20 17:07:23 2006 +0200
+++ b/doc-src/IsarRef/generic.tex	Fri Oct 20 17:07:24 2006 +0200
@@ -433,7 +433,8 @@
 A special case of locales are type classes.
 Type classes
 consist of a locale with \emph{exactly one} type variable
-and an corresponding axclass.
+and an corresponding axclass. \cite{isabelle-classes} gives a substantial
+introduction on type classes.
 
 \indexisarcmd{instance}\indexisarcmd{class}\indexisarcmd{print-classes}
 \begin{matharray}{rcl}
@@ -1331,7 +1332,7 @@
 \begin{descr}
 
 \item [$\isarcmd{print_claset}$] prints the collection of rules declared to
-  the Classical Reasoner, which is also known as ``simpset'' internally
+  the Classical Reasoner, which is also known as ``claset'' internally
   \cite{isabelle-ref}.  This is a diagnostic command; $undo$ does not apply.
   
 \item [$intro$, $elim$, and $dest$] declare introduction, elimination, and