src/HOL/Orderings.thy
changeset 29686 4cd2874eb5ff
parent 29580 117b88da143c
child 29823 0ab754d13ccd