src/Pure/General/queue.ML
changeset 64224 3ed43cfc8b14
parent 47060 e2741ec9ae36
equal deleted inserted replaced
64223:9d5b9f41df77 64224:3ed43cfc8b14