src/Pure/System/message_channel.ML
changeset 79401 6e6f76c5dd96
parent 78753 f40b59292288
child 80505 e3af424fdd1a