diff -r 96cf8edb6249 -r 62e0f892e525 doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex
--- a/doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex	Thu Jan 01 21:28:38 2009 +0100
+++ b/doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex	Thu Jan 01 21:30:13 2009 +0100
@@ -681,8 +681,8 @@
 %
 \isatagquote
 \isacommand{interpretation}\isamarkupfalse%
-\ idem{\isacharunderscore}class{\isacharcolon}\isanewline
-\ \ idem\ {\isacharbrackleft}{\isachardoublequoteopen}f\ {\isasymColon}\ {\isacharparenleft}{\isasymalpha}{\isasymColon}idem{\isacharparenright}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}{\isacharbrackright}\isanewline
+\ idem{\isacharunderscore}class{\isacharprime}{\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}%
@@ -843,7 +843,7 @@
 \endisadelimquote
 %
 \isatagquote
-\isacommand{interpretation}\isamarkupfalse%
+\isacommand{class{\isacharunderscore}interpretation}\isamarkupfalse%
 \ list{\isacharunderscore}monoid{\isacharcolon}\ monoid\ {\isacharbrackleft}append\ {\isachardoublequoteopen}{\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}{\isacharbrackright}\isanewline
 \ \ \isacommand{proof}\isamarkupfalse%
 \ \isacommand{qed}\isamarkupfalse%
@@ -874,12 +874,12 @@
 \ \ {\isachardoublequoteopen}replicate\ {\isadigit{0}}\ {\isacharunderscore}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
 \ \ {\isacharbar}\ {\isachardoublequoteopen}replicate\ {\isacharparenleft}Suc\ n{\isacharparenright}\ xs\ {\isacharequal}\ xs\ {\isacharat}\ replicate\ n\ xs{\isachardoublequoteclose}\isanewline
 \isanewline
-\isacommand{interpretation}\isamarkupfalse%
+\isacommand{class{\isacharunderscore}interpretation}\isamarkupfalse%
 \ list{\isacharunderscore}monoid{\isacharcolon}\ monoid\ {\isacharbrackleft}append\ {\isachardoublequoteopen}{\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}{\isacharbrackright}\ \isakeyword{where}\isanewline
 \ \ {\isachardoublequoteopen}monoid{\isachardot}pow{\isacharunderscore}nat\ append\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ replicate{\isachardoublequoteclose}\isanewline
 \isacommand{proof}\isamarkupfalse%
 \ {\isacharminus}\isanewline
-\ \ \isacommand{interpret}\isamarkupfalse%
+\ \ \isacommand{class{\isacharunderscore}interpret}\isamarkupfalse%
 \ monoid\ {\isacharbrackleft}append\ {\isachardoublequoteopen}{\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}{\isacharbrackright}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
 \isanewline
 \ \ \isacommand{show}\isamarkupfalse%
@@ -1231,7 +1231,7 @@
 \hspace*{0pt}\\
 \hspace*{0pt}fun inverse{\char95}int i = IntInf.{\char126}~i;\\
 \hspace*{0pt}\\
-\hspace*{0pt}val neutral{\char95}int :~IntInf.int = (0 :~IntInf.int);\\
+\hspace*{0pt}val neutral{\char95}int :~IntInf.int = (0 :~IntInf.int)\\
 \hspace*{0pt}\\
 \hspace*{0pt}fun mult{\char95}int i j = IntInf.+ (i,~j);\\
 \hspace*{0pt}\\
@@ -1258,7 +1258,7 @@
 \hspace*{0pt} ~~~else inverse A{\char95}~(pow{\char95}nat (monoid{\char95}group A{\char95}) (nat (IntInf.{\char126}~k)) x));\\
 \hspace*{0pt}\\
 \hspace*{0pt}val example :~IntInf.int =\\
-\hspace*{0pt} ~pow{\char95}int group{\char95}int (10 :~IntInf.int) ({\char126}2 :~IntInf.int);\\
+\hspace*{0pt} ~pow{\char95}int group{\char95}int (10 :~IntInf.int) ({\char126}2 :~IntInf.int)\\
 \hspace*{0pt}\\
 \hspace*{0pt}end;~(*struct Example*)%
 \end{isamarkuptext}%