src/Pure/General/queue.ML
changeset 48542 0a5f598cacec
parent 47060 e2741ec9ae36
equal deleted inserted replaced
48541:f31ef1a0285a 48542:0a5f598cacec