doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex
changeset 22385 cc2be3315e72
parent 22292 3b118010ec08
child 22479 de15ea8fb348
equal deleted inserted replaced
22384:33a46e6c7f04 22385:cc2be3315e72
   983 %
   983 %
   984 \isadelimML
   984 \isadelimML
   985 %
   985 %
   986 \endisadelimML
   986 \endisadelimML
   987 \isanewline
   987 \isanewline
   988 \isacommand{axclass}\isamarkupfalse%
   988 \isacommand{class}\isamarkupfalse%
   989 \ eq\ {\isasymsubseteq}\ type\isanewline
   989 \ eq\ {\isacharparenleft}\isakeyword{attach}\ {\isachardoublequoteopen}op\ {\isacharequal}{\isachardoublequoteclose}{\isacharparenright}\ {\isacharequal}\ \isakeyword{notes}\ reflexive%
   990 \ \ {\isacharparenleft}\isakeyword{attach}\ {\isachardoublequoteopen}op\ {\isacharequal}{\isachardoublequoteclose}{\isacharparenright}%
       
   991 \begin{isamarkuptext}%
   990 \begin{isamarkuptext}%
   992 This merely introduces a class \isa{eq} with corresponding
   991 This merely introduces a class \isa{eq} with corresponding
   993   operation \isa{op\ {\isacharequal}};
   992   operation \isa{op\ {\isacharequal}};
   994   the preprocessing framework does the rest.%
   993   the preprocessing framework does the rest.%
   995 \end{isamarkuptext}%
   994 \end{isamarkuptext}%