| changeset 62058 | 1cfd5d604937 |
| parent 61925 | ab52f183f020 |
| 62057:af58628952f0 | 62058:1cfd5d604937 |
|---|---|
1 (* Title: Pure/ML/ml_compiler_parameters_polyml-5.6.ML |
1 (* Title: Pure/RAW/ml_compiler_parameters_polyml-5.6.ML |
2 Author: Makarius |
2 Author: Makarius |
3 |
3 |
4 Additional ML compiler parameters for Poly/ML 5.6, or later. |
4 Additional ML compiler parameters for Poly/ML 5.6, or later. |
5 *) |
5 *) |
6 |
6 |