src/Pure/General/queue.ML
changeset 54247 81ee85f56e2d
parent 47060 e2741ec9ae36
equal deleted inserted replaced
54246:8fdb4dc08ed1 54247:81ee85f56e2d