src/HOL/Orderings.thy
changeset 24485 687bbb686ef9
parent 24422 c0b5ff9e9e4d
child 24641 448edc627ee4