src/HOL/Ord.thy
changeset 2638 6c6a44b5f757
parent 2624 ab311b6e5e29
child 3143 d60e49b86c6a