src/HOL/Ord.thy
changeset 4255 63ab0616900b
parent 3947 eb707467f8c5
child 4640 ac6cf9f18653