src/Pure/System/message_channel.ML
changeset 80749 232a839ef8e6
parent 80505 e3af424fdd1a
equal deleted inserted replaced
80748:43c4817375bf 80749:232a839ef8e6