src/HOL/Orderings.thy
changeset 28263 69eaa97e7e96
parent 27823 52971512d1a2
child 28516 e6fdcaaadbd3