src/Pure/General/ord_list.ML
changeset 27885 76b51cd0a37c
parent 22364 ddb91c9eb0fc
child 28354 c5fe7372ae4e