changeset 62058 | 1cfd5d604937 |
parent 61925 | ab52f183f020 |
--- a/src/Pure/RAW/ml_compiler_parameters.ML Tue Jan 05 13:41:29 2016 +0100 +++ b/src/Pure/RAW/ml_compiler_parameters.ML Tue Jan 05 13:48:51 2016 +0100 @@ -1,4 +1,4 @@ -(* Title: Pure/ML/ml_compiler_parameters.ML +(* Title: Pure/RAW/ml_compiler_parameters.ML Author: Makarius Additional ML compiler parameters for Poly/ML.