src/Pure/General/ord_list.ML
changeset 66660 bc3584f7ac0c
parent 44334 605381e7c7c5
equal deleted inserted replaced
66659:d5bf4bdb4fb7 66660:bc3584f7ac0c