src/Pure/System/message_channel.ML
changeset 67405 e9ab4ad7bd15
parent 62359 6709e51d5c11
child 69449 b516fdf8005c
equal deleted inserted replaced
67404:e128ab544996 67405:e9ab4ad7bd15