changeset 28255 | 6faea8ad8559 |
parent 28153 | 67147cc3f967 |
child 28268 | ac8431ecd57e |
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"; |