--- a/doc-src/AxClass/generated/Semigroups.tex Sun May 21 14:49:28 2000 +0200
+++ b/doc-src/AxClass/generated/Semigroups.tex Sun May 21 21:48:39 2000 +0200
@@ -1,24 +1,16 @@
\begin{isabelle}%
-\isacommand{theory}~Semigroups~=~Main:%
-\begin{isamarkuptext}%
-\noindent Associativity of binary operations:%
-\end{isamarkuptext}%
+\isacommand{theory}~Semigroups~=~Main:\isanewline
+\isanewline
\isacommand{constdefs}\isanewline
~~is\_assoc~::~{"}('a~{\isasymRightarrow}~'a~{\isasymRightarrow}~'a)~{\isasymRightarrow}~bool{"}\isanewline
-~~{"}is\_assoc~f~==~{\isasymforall}x~y~z.~f~(f~x~y)~z~=~f~x~(f~y~z){"}%
-\begin{isamarkuptext}%
-\medskip\noindent Semigroups over \isa{(op~{\isasymOplus})}:
- %term (latex xsymbols symbols) "op \<Oplus>";%
-\end{isamarkuptext}%
+~~{"}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}){"}%
-\begin{isamarkuptext}%
-\medskip\noindent Semigroups over \isa{(op~{\isasymOtimes})}:
- %term (latex xsymbols symbols) "op \<Otimes>";%
-\end{isamarkuptext}%
+~~assoc:~{"}is\_assoc~(op~{\isasymOplus}){"}\isanewline
+\isanewline
\isacommand{consts}\isanewline
~~times~::~{"}'a~{\isasymRightarrow}~'a~{\isasymRightarrow}~'a{"}~~~~(\isakeyword{infixl}~{"}{\isasymOtimes}{"}~65)\isanewline
\isacommand{axclass}\isanewline