summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

src/HOL/Isar_examples/Group.thy

changeset 7005 | cc778d613217 |

parent 6908 | 1bf0590f4790 |

child 7133 | 64c9f2364dae |

--- a/src/HOL/Isar_examples/Group.thy Wed Jul 14 13:06:08 1999 +0200 +++ b/src/HOL/Isar_examples/Group.thy Wed Jul 14 13:07:09 1999 +0200 @@ -128,7 +128,7 @@ monoid_right_unit: "x * one = x"; text {* - Groups are *not* yet monoids directly from the definition . For + Groups are *not* yet monoids directly from the definition. For monoids, right_unit had to be included as an axiom, but for groups both right_unit and right_inverse are derivable from the other axioms. With group_right_unit derived as a theorem of group theory