including polyml-time-limit.ML
authorwebertj
Tue, 01 Jun 2004 00:18:01 +0200
changeset 14850 393a7be73160
parent 14849 73a0a6e0426a
child 14851 0fc75361e0c7
including polyml-time-limit.ML
src/Pure/ML-Systems/polyml.ML
--- a/src/Pure/ML-Systems/polyml.ML	Tue Jun 01 00:17:07 2004 +0200
+++ b/src/Pure/ML-Systems/polyml.ML	Tue Jun 01 00:18:01 2004 +0200
@@ -30,6 +30,10 @@
 
 use "ML-Systems/cpu-timer-basis.ML";
 
+(* bounded time execution *)
+
+use "ML-Systems/polyml-time-limit.ML";
+
 (* prompts *)
 
 fun ml_prompts p1 p2 = (PolyML.Compiler.prompt1 := p1; PolyML.Compiler.prompt2 := p2);