--- a/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex Fri Mar 02 15:43:15 2007 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex Fri Mar 02 15:43:16 2007 +0100
@@ -985,9 +985,8 @@
%
\endisadelimML
\isanewline
-\isacommand{axclass}\isamarkupfalse%
-\ eq\ {\isasymsubseteq}\ type\isanewline
-\ \ {\isacharparenleft}\isakeyword{attach}\ {\isachardoublequoteopen}op\ {\isacharequal}{\isachardoublequoteclose}{\isacharparenright}%
+\isacommand{class}\isamarkupfalse%
+\ eq\ {\isacharparenleft}\isakeyword{attach}\ {\isachardoublequoteopen}op\ {\isacharequal}{\isachardoublequoteclose}{\isacharparenright}\ {\isacharequal}\ \isakeyword{notes}\ reflexive%
\begin{isamarkuptext}%
This merely introduces a class \isa{eq} with corresponding
operation \isa{op\ {\isacharequal}};