src/HOL/Ord.thy
changeset 6017 dbb33359a7ab
parent 5953 d6017ce6b93e
child 6402 2b23e14dd386