src/Pure/System/system_channel.ML
changeset 48275 31daac3a85ea
parent 45158 db4bf4fb5492
child 50800 c0fb2839d1a9
equal deleted inserted replaced
48274:c8dce1689f79 48275:31daac3a85ea