src/HOL/Orderings.thy
changeset 38794 2d638e963357
parent 38786 e46e7a9cb622
child 38795 848be46708dc