src/HOL/Orderings.thy
changeset 33242 99577c7085c8
parent 32960 69916a850301
child 33519 e31a85f92ce9