src/HOL/OrderedGroup.ML
changeset 21404 eb85850d3eb7
parent 20713 823967ef47f1