src/HOL/OrderedGroup.ML
changeset 15195 197e00ce3f20
parent 14755 5cc6e6b9e27a
child 16423 24abe4c0e4b4