src/HOL/Orderings.thy
changeset 42817 7e819eb7dabb
parent 42795 66fcc9882784
child 43596 78211f66cf8d