| changeset 33538 | edf497b5b5d2 |
| parent 32738 | 15bb09ca0378 |
| child 38470 | 484e483eb606 |
| 33537:06c87d2c5b5a | 33538:edf497b5b5d2 |
|---|---|
1 (* Title: Pure/ML-Systems/compiler_polyml-5.3.ML |
1 (* Title: Pure/ML-Systems/compiler_polyml-5.3.ML |
2 |
2 |
3 Runtime compilation for Poly/ML 5.3. |
3 Runtime compilation for Poly/ML 5.3.0. |
4 *) |
4 *) |
5 |
5 |
6 local |
6 local |
7 |
7 |
8 fun drop_newline s = |
8 fun drop_newline s = |