src/HOL/Ord.thy
changeset 1334 32a9fde85699
parent 965 24eef3860714
child 1370 7361ac9b024d