src/HOL/OrderedGroup.ML
changeset 20604 9dba9c7872c9
parent 20129 95e84d2c9f2c
child 20713 823967ef47f1