src/HOL/OrderedGroup.ML
changeset 15140 322485b816ac
parent 14755 5cc6e6b9e27a
child 16423 24abe4c0e4b4