[Hol-info] polyml thread support

[Lu Z. <lu...@cs...>]

Hey,

Can I use the thread support in PolyML to do this task? and how? I'd
like to run a ML function, which runs a HOL proof, for a certain amount
of time, say 20 seconds, and if the function hasn't terminated by this
time limit, I want to kill that thread and run the same function again
with a different parameter. If the thread terminates before the time
limit, then it reports to its parent thread so that the parent can stop
the timer and execute another function.

Thanks a lot.
Lu