# HG changeset patch
# User wenzelm
# Date 963523404 -7200
# Node ID 3da45f19730e4c54f04364290261dac014304f6b
# Parent  6861e3b00155f86a8dcda24621dca9fbde13a7f5
updated;

diff -r 6861e3b00155 -r 3da45f19730e doc-src/AxClass/generated/Group.tex
--- 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
diff -r 6861e3b00155 -r 3da45f19730e doc-src/AxClass/generated/Product.tex
--- 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