src/HOL/Ord.thy
changeset 2981 aa5aeb6467c6
parent 2624 ab311b6e5e29
child 3143 d60e49b86c6a