src/Pure/Concurrent/multithreading.ML
Wed, 09 May 2018 20:45:57 +0200 wenzelm clarified future scheduling parameters, with support for parallel_limit;
Tue, 24 Apr 2018 11:03:51 +0200 wenzelm clarified modules;
Mon, 19 Feb 2018 11:13:25 +0100 wenzelm clarified signature;
Wed, 14 Dec 2016 10:40:25 +0100 wenzelm tuned;
Wed, 14 Dec 2016 10:29:47 +0100 wenzelm tuned;
Tue, 13 Dec 2016 23:29:54 +0100 wenzelm more tight thread attributes, based in internal word arithmetic instead of symbolic datatypes: measurable performance improvement;
Mon, 17 Oct 2016 16:58:39 +0200 wenzelm eliminated unused argument;
less more (0) -10 -7 tip