src/Pure/General/ord_list.ML
changeset 83011 d35875d530a2
parent 44334 605381e7c7c5
equal deleted inserted replaced
83010:b01548bf9e77 83011:d35875d530a2