summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

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. *}