# HG changeset patch
# User wenzelm
# Date 958989923 -7200
# Node ID 981ac87f905c23fb4e57d9c40dd04dc8aec51813
# Parent  96503b90307b67333950d4bbe629a51b08d4a864
tuned;

diff -r 96503b90307b -r 981ac87f905c src/HOL/Isar_examples/Group.thy
--- a/src/HOL/Isar_examples/Group.thy	Mon May 22 12:05:12 2000 +0200
+++ b/src/HOL/Isar_examples/Group.thy	Mon May 22 12:05:23 2000 +0200
@@ -35,7 +35,7 @@
 proof -;
   have "x * inv x = one * (x * inv x)";
     by (simp only: group_left_unit);
-  also; have "... = (one * x) * inv x";
+  also; have "... = one * x * inv x";
     by (simp only: group_assoc);
   also; have "... = inv (inv x) * inv x * x * inv x";
     by (simp only: group_left_inverse);