diff -r 33a46e6c7f04 -r cc2be3315e72 doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex
--- 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}};