src/HOL/AxClasses/Lattice/OrdDefs.thy
changeset 1465 5d7a7e439cec
parent 1440 de6f18da81bb
child 1476 608483c2122a