src/HOL/Orderings.thy
changeset 82407 fcc0f74ac086
parent 82026 57b4e44f5bc4
child 82593 88043331f166