src/HOL/OrderedGroup.ML
changeset 21542 4462ee172ef0
parent 20713 823967ef47f1