src/HOL/Ord.ML
changeset 5253 82a5ca6290aa
parent 5143 b94cd208f073
child 5316 7a8975451a89