src/Pure/Concurrent/mailbox.ML
changeset 80453 7a2d9e3fcdd5
parent 62826 eb94e570c1a4
equal deleted inserted replaced
80452:0303b3a0edde 80453:7a2d9e3fcdd5