src/HOL/Ord.thy
changeset 2212 bd705e9de196
parent 2006 72754e060aa2
child 2259 e6d738f2b9a9