src/HOL/Ord.ML
changeset 4724 3d2375efb80e
parent 4686 74a12e86b20b
child 5069 3ea049f7979d