src/HOL/Orderings.thy
changeset 25577 d739f48ef40c
parent 25510 38c15efe603b
child 25614 0b8baa94b866