src/HOL/OrderedGroup.ML
changeset 21977 7f7177a95189
parent 20713 823967ef47f1