src/HOL/Orderings.ML
changeset 21391 a8809f46bd7f
parent 21216 1c8580913738
child 21619 dea0914773f7