--- 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}%
%