changeset 8910 | 981ac87f905c |
parent 7982 | d534b897ce39 |
child 10007 | 64bf7da1994a |
--- 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);