src/HOL/OrderedGroup.ML
changeset 14890 51f28df21c8b
parent 14755 5cc6e6b9e27a
child 16423 24abe4c0e4b4