src/Pure/General/queue.ML
changeset 78982 be5c078f5292
parent 47060 e2741ec9ae36
equal deleted inserted replaced
78981:47f8533c6887 78982:be5c078f5292