| changeset 41717 | 8a1ab91df301 |
| parent 39242 | 28d3809ff91f |
| 41716:4b08499b3db1 | 41717:8a1ab91df301 |
|---|---|
1 (* Title: Pure/ML-Systems/compiler_polyml-5.2.ML |
1 (* Title: Pure/ML-Systems/compiler_polyml-5.2.ML |
2 |
2 |
3 Runtime compilation for Poly/ML 5.2 and 5.2.1. |
3 Runtime compilation for Poly/ML 5.2.x. |
4 *) |
4 *) |
5 |
5 |
6 local |
6 local |
7 |
7 |
8 fun drop_newline s = |
8 fun drop_newline s = |