| changeset 25613 | bd055df900d3 |
| parent 25512 | 4134f7c782e2 |
| child 25762 | c03e9d04b3e4 |
--- a/src/HOL/OrderedGroup.thy Thu Dec 13 07:09:00 2007 +0100 +++ b/src/HOL/OrderedGroup.thy Thu Dec 13 07:09:01 2007 +0100 @@ -80,7 +80,7 @@ begin subclass monoid_mult - by unfold_locales (insert mult_1, simp_all add: mult_commute) + by unfold_locales (insert mult_1, simp_all add: mult_commute) end