src/Pure/System/message_channel.ML
changeset 54381 9c1f21365326
parent 52800 1baa5d19ac44
child 56333 38f1422ef473