src/HOL/Ord.ML
changeset 4200 5a2cd204f8b4
parent 4089 96fba19bcbe2
child 4600 e3e7e901ce6c
equal deleted inserted replaced
4199:2b9fc1f08886 4200:5a2cd204f8b4