src/Pure/ML-Systems/polyml.ML
changeset 28255 6faea8ad8559
parent 28153 67147cc3f967
child 28268 ac8431ecd57e
equal deleted inserted replaced
28254:d67ba23e0277 28255:6faea8ad8559
     1 (*  Title:      Pure/ML-Systems/polyml.ML
     1 (*  Title:      Pure/ML-Systems/polyml.ML
     2     ID:         $Id$
     2     ID:         $Id$
     3 
     3 
     4 Compatibility wrapper for Poly/ML (after 5.1).
     4 Compatibility wrapper for Poly/ML 5.2 or later.
     5 *)
     5 *)
     6 
     6 
     7 open Thread;
     7 open Thread;
     8 use "ML-Systems/polyml_common.ML";
     8 use "ML-Systems/polyml_common.ML";
     9 use "ML-Systems/multithreading_polyml.ML";
     9 use "ML-Systems/multithreading_polyml.ML";