src/Pure/General/ord_list.ML
changeset 28732 99492b224b7b
parent 28626 f65736dfc40d
child 29606 fedb8be05f24