src/Pure/Concurrent/future.ML
changeset 74338 534b231ce041
parent 74166 ff3dbb2be924
child 78648 852ec09aef13
equal deleted inserted replaced
74337:9c1ad2f04660 74338:534b231ce041