src/Pure/System/message_channel.ML
changeset 68220 8fc4e3d1df86
parent 62359 6709e51d5c11
child 69449 b516fdf8005c