| changeset 29564 | f8b933a62151 |
| parent 28267 | 596b0fd784a3 |
| child 30671 | 2f64540707d6 |
| 29563:4773c5c994dc | 29564:f8b933a62151 |
|---|---|
1 (* Title: Pure/ML-Systems/ml_name_space.ML |
1 (* Title: Pure/ML-Systems/ml_name_space.ML |
2 ID: $Id$ |
|
3 Author: Makarius |
2 Author: Makarius |
4 |
3 |
5 ML name space -- dummy version of Poly/ML 5.2 facility. |
4 ML name space -- dummy version of Poly/ML 5.2 facility. |
6 *) |
5 *) |
7 |
6 |