src/HOL/Ord.ML
changeset 4628 0c7e97836e3c
parent 4600 e3e7e901ce6c
child 4640 ac6cf9f18653
equal deleted inserted replaced
4627:ae95666c71cc 4628:0c7e97836e3c