src/HOL/OrderedGroup.ML
changeset 14898 a25550451b51
parent 14755 5cc6e6b9e27a
child 16423 24abe4c0e4b4