src/HOL/OrderedGroup.ML
changeset 20192 956cd30ef3be
parent 20129 95e84d2c9f2c
child 20713 823967ef47f1