1 (* Title: Pure/ML/ml_debugger.ML
1 (* Title: Pure/RAW/ml_debugger.ML
2 Author: Makarius
3
4 ML debugger interface -- dummy version.
5 *)
6