src/Pure/System/system_channel.ML
changeset 48710 5b51ccdc8623
parent 45158 db4bf4fb5492
child 50800 c0fb2839d1a9