src/HOL/Ord.thy
changeset 2351 873ffd6f70c3
parent 2259 e6d738f2b9a9
child 2608 450c9b682a92