src/HOL/Orderings.thy
changeset 69272 15e9ed5b28fb
parent 67673 c8caefb20564
child 69593 3dda49e08b9d