src/HOL/Ord.thy
changeset 4386 b3cff8adc213
parent 3947 eb707467f8c5
child 4640 ac6cf9f18653