src/Pure/General/queue.ML
changeset 40650 d40b347d5b0b
parent 29606 fedb8be05f24
child 47060 e2741ec9ae36
equal deleted inserted replaced
40649:dc1b5aa908ff 40650:d40b347d5b0b