src/HOL/AxClasses/Lattice/OrdDefs.thy
changeset 8516 f5f6a97ee43f
parent 1476 608483c2122a