src/HOL/Ord.thy
changeset 1072 0140ff702b23
parent 965 24eef3860714
child 1370 7361ac9b024d