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