changeset 62874 | b0194643e64c |
parent 62870 | cf724647f75b |
child 62878 | 1cec457e0a03 |
62873:2f9c8a18f832 | 62874:b0194643e64c |
---|---|
333 use_no_debug "Tools/debugger.ML"; |
333 use_no_debug "Tools/debugger.ML"; |
334 use "Tools/named_theorems.ML"; |
334 use "Tools/named_theorems.ML"; |
335 use "Tools/jedit.ML"; |
335 use "Tools/jedit.ML"; |
336 |
336 |
337 use_thy "Pure"; |
337 use_thy "Pure"; |
338 |
|
339 use "ML/ml_pervasive_final.ML"; |
|
338 use_thy "ML/ML_Root"; |
340 use_thy "ML/ML_Root"; |
339 |
|
340 use "ML/ml_pervasive_final.ML"; |