src/HOL/Ord.thy
changeset 6179 e40b647fd6d0
parent 5953 d6017ce6b93e
child 6402 2b23e14dd386