\begin{isabelle}%
\isacommand{theory}~Semigroups~=~Main:\isanewline
\isanewline
\isacommand{constdefs}\isanewline
~~is\_assoc~::~{"}('a~{\isasymRightarrow}~'a~{\isasymRightarrow}~'a)~{\isasymRightarrow}~bool{"}\isanewline
~~{"}is\_assoc~f~{\isasymequiv}~{\isasymforall}x~y~z.~f~(f~x~y)~z~=~f~x~(f~y~z){"}\isanewline
\isanewline
\isacommand{consts}\isanewline
~~plus~::~{"}'a~{\isasymRightarrow}~'a~{\isasymRightarrow}~'a{"}~~~~(\isakeyword{infixl}~{"}{\isasymOplus}{"}~65)\isanewline
\isacommand{axclass}\isanewline
~~plus\_semigroup~<~{"}term{"}\isanewline
~~assoc:~{"}is\_assoc~(op~{\isasymOplus}){"}\isanewline
\isanewline
\isacommand{consts}\isanewline
~~times~::~{"}'a~{\isasymRightarrow}~'a~{\isasymRightarrow}~'a{"}~~~~(\isakeyword{infixl}~{"}{\isasymOtimes}{"}~65)\isanewline
\isacommand{axclass}\isanewline
~~times\_semigroup~<~{"}term{"}\isanewline
~~assoc:~{"}is\_assoc~(op~{\isasymOtimes}){"}\isanewline
\isanewline
\isacommand{end}\end{isabelle}%