src/Pure/RAW/ml_debugger.ML
changeset 62058 1cfd5d604937
parent 61925 ab52f183f020
equal deleted inserted replaced
62057:af58628952f0 62058:1cfd5d604937
     1 (*  Title:      Pure/ML/ml_debugger.ML
     1 (*  Title:      Pure/RAW/ml_debugger.ML
     2     Author:     Makarius
     2     Author:     Makarius
     3 
     3 
     4 ML debugger interface -- dummy version.
     4 ML debugger interface -- dummy version.
     5 *)
     5 *)
     6 
     6