src/Pure/General/ord_list.ML
changeset 23239 3648e97da60b
parent 22364 ddb91c9eb0fc
child 28354 c5fe7372ae4e