src/Pure/ML-Systems/time_limit.ML
Mon, 24 Sep 2007 13:52:50 +0200 wenzelm replaced interrupt_timeout by TimeLimit.timeLimit (available on SML/NJ and Poly/ML 5.1);
less more (0) tip