src/HOL/Orderings.ML
changeset 21542 4462ee172ef0
parent 21216 1c8580913738
child 21619 dea0914773f7