src/HOL/Ord.ML
changeset 10430 d3f780c3af0c
parent 10231 178a272bceeb
child 10753 e43e017df8c1
equal deleted inserted replaced
10429:8820f787e61e 10430:d3f780c3af0c