--- a/doc-src/AxClass/generated/Group.tex Thu Jul 13 23:22:26 2000 +0200
+++ b/doc-src/AxClass/generated/Group.tex Thu Jul 13 23:23:24 2000 +0200
@@ -214,7 +214,7 @@
exclusive-or as operation $\TIMES$, identity as $\isasyminv$, and
$False$ as $1$ forms an Abelian group.%
\end{isamarkuptext}%
-\isacommand{defs}\isanewline
+\isacommand{defs}~(\isakeyword{overloaded})\isanewline
~~times\_bool\_def:~~~{"}x~{\isasymOtimes}~y~{\isasymequiv}~x~{\isasymnoteq}~(y{\isasymColon}bool){"}\isanewline
~~inverse\_bool\_def:~{"}x{\isasyminv}~{\isasymequiv}~x{\isasymColon}bool{"}\isanewline
~~unit\_bool\_def:~~~~{"}{\isasymunit}~{\isasymequiv}~False{"}%
@@ -269,7 +269,7 @@
products, direct sums or function spaces. Subsequently we lift
$\TIMES$ component-wise to binary products $\alpha \times \beta$.%
\end{isamarkuptext}%
-\isacommand{defs}\isanewline
+\isacommand{defs}~(\isakeyword{overloaded})\isanewline
~~times\_prod\_def:~{"}p~{\isasymOtimes}~q~{\isasymequiv}~(fst~p~{\isasymOtimes}~fst~q,~snd~p~{\isasymOtimes}~snd~q){"}%
\begin{isamarkuptext}%
It is very easy to see that associativity of $\TIMES^\alpha$ and
--- a/doc-src/AxClass/generated/Product.tex Thu Jul 13 23:22:26 2000 +0200
+++ b/doc-src/AxClass/generated/Product.tex Thu Jul 13 23:23:24 2000 +0200
@@ -50,7 +50,7 @@
\end{isamarkuptext}%
\isacommand{instance}~bool~::~product\isanewline
~~\isacommand{by}~intro\_classes\isanewline
-\isacommand{defs}\isanewline
+\isacommand{defs}~(\isakeyword{overloaded})\isanewline
~~product\_bool\_def:~{"}x~{\isasymOtimes}~y~{\isasymequiv}~x~{\isasymand}~y{"}%
\begin{isamarkuptext}%
The definition $prod_bool_def$ becomes syntactically well-formed only