src/HOL/OrderedGroup.ML
changeset 21316 4d913b8bccf1
parent 20713 823967ef47f1