src/Pure/net.ML
changeset 41686 d8efc2490b8e
parent 37523 40c352510065
child 45404 69ec395ef6ca
equal deleted inserted replaced
41685:e29ea98a76ce 41686:d8efc2490b8e