src/HOL/OrderedGroup.ML
changeset 22320 d5260836d662
parent 20713 823967ef47f1