# HG changeset patch
# User wenzelm
# Date 965379562 -7200
# Node ID 0c8422ed066fdabd8e830a07db22482aafdac8f1
# Parent  f58863b1406a6af727c1612a1e159c056ea0552c
tuned;

diff -r f58863b1406a -r 0c8422ed066f doc-src/AxClass/Group/Group.thy
--- 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.
 *}