changeset 31433 | 12f5f6af3d2d |
parent 31427 | 5a07cc86675d |
child 32776 | 1504f9c2d060 |
31432:9858f32f9569 | 31433:12f5f6af3d2d |
---|---|
1 (* Title: Pure/ML-Systems/polyml-experimental.ML |
1 (* Title: Pure/ML-Systems/polyml-experimental.ML |
2 |
2 |
3 Compatibility wrapper for Poly/ML 5.3 (SVN experimental). |
3 Compatibility wrapper for Poly/ML 5.3. |
4 *) |
4 *) |
5 |
5 |
6 open Thread; |
6 open Thread; |
7 |
7 |
8 structure ML_Name_Space = |
8 structure ML_Name_Space = |