src/HOL/Orderings.thy
changeset 80987 e7a926b5b5be
parent 80934 8e72f55295fd
child 82026 57b4e44f5bc4