src/HOL/Orderings.thy
changeset 58446 e89f57d1e46c
parent 57447 87429bdecad5
child 58826 2ed2eaabe3df