author wenzelm Fri, 04 Aug 2000 10:59:22 +0200 changeset 9518 0c8422ed066f parent 9517 f58863b1406a child 9519 fdc3b5bcd79d
tuned;
--- a/doc-src/AxClass/Group/Group.thy	Thu Aug 03 19:29:03 2000 +0200
+++ b/doc-src/AxClass/Group/Group.thy	Fri Aug 04 10:59:22 2000 +0200
@@ -42,7 +42,7 @@
\noindent So class $monoid$ contains exactly those types $\tau$ where
$\TIMES :: \tau \To \tau \To \tau$ and $1 :: \tau$ are specified
appropriately, such that $\TIMES$ is associative and $1$ is a left
- and right unit element for $\TIMES$.
+ and right unit element for the $\TIMES$ operation.
*}

text {*
@@ -227,7 +227,7 @@
transferred to Isabelle's type signature level.

\medskip As a typical example, we show that type $bool$ with
- exclusive-or as operation $\TIMES$, identity as $\isasyminv$, and
+ exclusive-or as $\TIMES$ operation, identity as $\isasyminv$, and
$False$ as $1$ forms an Abelian group.
*}