src/Pure/System/message_channel.ML
changeset 70299 83774d669b51
parent 69451 387894c2fb2c
child 70995 2c17fa0f5187