src/HOL/Ord.ML
changeset 1294 1358dc040edb
parent 923 ff1574a81019
child 1465 5d7a7e439cec