equal
deleted
inserted
replaced
1 (* Title: Pure/Tools/value.ML |
1 (* Title: Tools/value.ML |
2 Author: Florian Haftmann, TU Muenchen |
2 Author: Florian Haftmann, TU Muenchen |
3 |
3 |
4 Generic value command for arbitrary evaluators. |
4 Generic value command for arbitrary evaluators. |
5 *) |
5 *) |
6 |
6 |