| changeset 31470 | 01e7a8bb9e5b |
| parent 31430 | 04192aa43112 |
| child 33519 | e31a85f92ce9 |
| 31469:40f815edbde4 | 31470:01e7a8bb9e5b |
|---|---|
1 (* Title: Pure/ML/ml_env.ML |
1 (* Title: Pure/ML/ml_env.ML |
2 Author: Makarius |
2 Author: Makarius |
3 |
3 |
4 Local environment of ML sources and results. |
4 Local environment of ML results. |
5 *) |
5 *) |
6 |
6 |
7 signature ML_ENV = |
7 signature ML_ENV = |
8 sig |
8 sig |
9 val inherit: Context.generic -> Context.generic -> Context.generic |
9 val inherit: Context.generic -> Context.generic -> Context.generic |