Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
defs (overloaded);
authorwenzelm
Thu, 13 Jul 2000 23:07:10 +0200
changeset 9306 d0ef4a41ae63
parent 9305 3dfae8f90dcf
child 9307 5613e184b8b3
defs (overloaded);
doc-src/AxClass/Group/Group.thy file | annotate | diff | comparison | revisions
doc-src/AxClass/Group/Product.thy file | annotate | diff | comparison | revisions 
--- 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 {*
--- 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 {*
isabelle