src/Pure/ML-Systems/multithreading_polyml.ML
changeset 31311 b82e55f51dcc
parent 30612 cb6421b6a18f
child 31630 2f8ed0dca3bd
equal deleted inserted replaced
31310:b5365a9db718 31311:b82e55f51dcc
     1 (*  Title:      Pure/ML-Systems/multithreading_polyml.ML
     1 (*  Title:      Pure/ML-Systems/multithreading_polyml.ML
     2     Author:     Makarius
     2     Author:     Makarius
     3 
     3 
     4 Multithreading in Poly/ML 5.2 or later (cf. polyml/basis/Thread.sml).
     4 Multithreading in Poly/ML 5.2.1 or later (cf. polyml/basis/Thread.sml).
     5 *)
     5 *)
     6 
     6 
     7 signature MULTITHREADING_POLYML =
     7 signature MULTITHREADING_POLYML =
     8 sig
     8 sig
     9   val interruptible: ('a -> 'b) -> 'a -> 'b
     9   val interruptible: ('a -> 'b) -> 'a -> 'b