src/HOL/OrderedGroup.ML
changeset 17517 9dc9d3005ed2
parent 16568 e02fe7ae212b
child 18925 2e3d508ba8dc