# HG changeset patch
# User wenzelm
# Date 963522430 -7200
# Node ID d0ef4a41ae6334a3c6ddc0ea032887b79c212dea
# Parent  3dfae8f90dcf2398e9d099a8cf0ff61b69aa62f9
defs (overloaded);

diff -r 3dfae8f90dcf -r d0ef4a41ae63 doc-src/AxClass/Group/Group.thy
--- a/doc-src/AxClass/Group/Group.thy	Thu Jul 13 13:05:58 2000 +0200
+++ b/doc-src/AxClass/Group/Group.thy	Thu Jul 13 23:07:10 2000 +0200
@@ -231,7 +231,7 @@
  $False$ as $1$ forms an Abelian group.
 *}
 
-defs
+defs (overloaded)
   times_bool_def:   "x \<Otimes> y \\<equiv> x \\<noteq> (y\\<Colon>bool)"
   inverse_bool_def: "x\<inv> \\<equiv> x\\<Colon>bool"
   unit_bool_def:    "\<unit> \\<equiv> False"
@@ -291,7 +291,7 @@
  $\TIMES$ component-wise to binary products $\alpha \times \beta$.
 *}
 
-defs
+defs (overloaded)
   times_prod_def: "p \<Otimes> q \\<equiv> (fst p \<Otimes> fst q, snd p \<Otimes> snd q)"
 
 text {*
diff -r 3dfae8f90dcf -r d0ef4a41ae63 doc-src/AxClass/Group/Product.thy
--- a/doc-src/AxClass/Group/Product.thy	Thu Jul 13 13:05:58 2000 +0200
+++ b/doc-src/AxClass/Group/Product.thy	Thu Jul 13 23:07:10 2000 +0200
@@ -54,7 +54,7 @@
 
 instance bool :: product
   by intro_classes
-defs
+defs (overloaded)
   product_bool_def: "x \\<Otimes> y \\<equiv> x \\<and> y"
 
 text {*