src/Pure/General/ord_list.ML
changeset 24854 0ebcd575d3c6
parent 22364 ddb91c9eb0fc
child 28354 c5fe7372ae4e