doc-src/AxClass/generated/Semigroup.tex

snapshot of new Isar'ized version;

\begin{isabelle}%
\isacommand{theory}~Semigroup~=~Main:\isanewline
\isanewline
\isacommand{consts}\isanewline
~~times~::~{"}'a~{\isasymRightarrow}~'a~{\isasymRightarrow}~'a{"}~~~~(\isakeyword{infixl}~{"}{\isasymOtimes}{"}~70)\isanewline
\isacommand{axclass}\isanewline
~~semigroup~<~{"}term{"}\isanewline
~~assoc:~{"}(x~{\isasymOtimes}~y)~{\isasymOtimes}~z~=~x~{\isasymOtimes}~(y~{\isasymOtimes}~z){"}\isanewline
\isanewline
\isacommand{end}\end{isabelle}%