author | webertj |
Tue, 01 Jun 2004 00:18:01 +0200 | |
changeset 14850 | 393a7be73160 |
parent 14849 | 73a0a6e0426a |
child 14851 | 0fc75361e0c7 |
--- 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);