src/Pure/Concurrent/bash.ML
Wed, 10 Aug 2011 15:17:24 +0200 wenzelm more explicit Simple_Thread.interrupt_unsynchronized, to emphasize its meaning;
Mon, 08 Aug 2011 13:40:24 +0200 wenzelm proper signature;
less more (0) -2 tip