| author | nipkow | 
| Sun, 28 Nov 2010 15:20:51 +0100 | |
| changeset 40786 | 0a54cfc9add3 | 
| parent 29564 | f8b933a62151 | 
| permissions | -rw-r--r-- | 
(* Title: Pure/ML-Systems/time_limit.ML Author: Makarius Dummy implementation of NJ's TimeLimit structure. *) signature TIME_LIMIT = sig exception TimeOut val timeLimit : Time.time -> ('a -> 'b) -> 'a -> 'b end; structure TimeLimit: TIME_LIMIT = struct exception TimeOut; fun timeLimit _ f x = f x; end;