--- a/doc-src/AxClass/generated/Semigroups.tex Mon May 22 10:31:44 2000 +0200
+++ b/doc-src/AxClass/generated/Semigroups.tex Mon May 22 11:56:55 2000 +0200
@@ -4,12 +4,12 @@
\isacommand{theory}~Semigroups~=~Main:%
\begin{isamarkuptext}%
\medskip\noindent An axiomatic type class is simply a class of types
- that all meet certain \emph{axioms}. Thus, type classes may be also
- understood as type predicates --- i.e.\ abstractions over a single
- type argument $\alpha$. Class axioms typically contain polymorphic
- constants that depend on this type $\alpha$. These
- \emph{characteristic constants} behave like operations associated
- with the ``carrier'' type $\alpha$.
+ that all meet certain properties, which are also called \emph{class
+ axioms}. Thus, type classes may be also understood as type predicates
+ --- i.e.\ abstractions over a single type argument $\alpha$. Class
+ axioms typically contain polymorphic constants that depend on this
+ type $\alpha$. These \emph{characteristic constants} behave like
+ operations associated with the ``carrier'' type $\alpha$.
We illustrate these basic concepts by the following formulation of
semigroups.%
@@ -32,8 +32,8 @@
\medskip In general, type classes may be used to describe
\emph{structures} with exactly one carrier $\alpha$ and a fixed
\emph{signature}. Different signatures require different classes.
- Subsequently, class $plus_semigroup$ represents semigroups of the
- form $(\tau, \PLUS^\tau)$, while $semigroup$ above would correspond
+ Below, class $plus_semigroup$ represents semigroups of the form
+ $(\tau, \PLUS^\tau)$, while the original $semigroup$ would correspond
to semigroups $(\tau, \TIMES^\tau)$.%
\end{isamarkuptext}%
\isacommand{consts}\isanewline
@@ -42,7 +42,8 @@
~~plus\_semigroup~<~{"}term{"}\isanewline
~~assoc:~{"}(x~{\isasymOplus}~y)~{\isasymOplus}~z~=~x~{\isasymOplus}~(y~{\isasymOplus}~z){"}%
\begin{isamarkuptext}%
-\noindent Even if classes $plus_semigroup$ and $times_semigroup$ both
- represent semigroups in a sense, they are certainly not the same!%
+\noindent Even if classes $plus_semigroup$ and $semigroup$ both
+ represent semigroups in a sense, they are certainly not quite the
+ same.%
\end{isamarkuptext}%
\isacommand{end}\end{isabelle}%