src/Pure/General/queue.ML
changeset 49467 25b7e843e124
parent 47060 e2741ec9ae36
equal deleted inserted replaced
49466:99ed1f422635 49467:25b7e843e124