src/HOL/Ord.ML
changeset 6833 15d6c121d75f
parent 6814 d96d4977f94e
child 6956 18c0457efd3d