src/HOL/Ord.thy
changeset 6378 5780d71203bb
parent 5953 d6017ce6b93e
child 6402 2b23e14dd386