src/HOL/Orderings.thy
changeset 60495 d7ff0a1df90a
parent 60097 d20ca79d50e4
child 60758 d8d85a8172b5