diff -r 206e2f1759cc -r 8fd9d555d04d doc-src/Classes/Thy/document/Classes.tex
--- a/doc-src/Classes/Thy/document/Classes.tex	Mon Feb 22 14:11:03 2010 +0100
+++ b/doc-src/Classes/Thy/document/Classes.tex	Mon Feb 22 17:02:39 2010 +0100
@@ -641,7 +641,7 @@
 %
 \begin{isamarkuptext}%
 \noindent The connection to the type system is done by means
-  of a primitive axclass%
+  of a primitive type class%
 \end{isamarkuptext}%
 \isamarkuptrue%
 \ %
@@ -663,9 +663,8 @@
 \endisadelimquote
 %
 \isatagquote
-\isacommand{axclass}\isamarkupfalse%
-\ idem\ {\isacharless}\ type\isanewline
-\ \ idem{\isacharcolon}\ {\isachardoublequoteopen}f\ {\isacharparenleft}f\ x{\isacharparenright}\ {\isacharequal}\ f\ x{\isachardoublequoteclose}\ %
+\isacommand{classes}\isamarkupfalse%
+\ idem\ {\isacharless}\ type%
 \endisatagquote
 {\isafoldquote}%
 %
@@ -698,10 +697,7 @@
 \isatagquote
 \isacommand{interpretation}\isamarkupfalse%
 \ idem{\isacharunderscore}class{\isacharcolon}\isanewline
-\ \ idem\ {\isachardoublequoteopen}f\ {\isasymColon}\ {\isacharparenleft}{\isasymalpha}{\isasymColon}idem{\isacharparenright}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\isanewline
-\isacommand{proof}\isamarkupfalse%
-\ \isacommand{qed}\isamarkupfalse%
-\ {\isacharparenleft}rule\ idem{\isacharparenright}%
+\ \ idem\ {\isachardoublequoteopen}f\ {\isasymColon}\ {\isacharparenleft}{\isasymalpha}{\isasymColon}idem{\isacharparenright}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}%
 \endisatagquote
 {\isafoldquote}%
 %