src/Pure/General/queue.ML
changeset 69450 b28b001e7ee8
parent 47060 e2741ec9ae36
equal deleted inserted replaced
69449:b516fdf8005c 69450:b28b001e7ee8