src/HOL/Ord.thy
changeset 11115 285b31e9e026
parent 10460 a8d9a79ed95e
child 11140 a46eaedbeb2d