--- 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