src/Pure/RAW/ml_compiler_parameters.ML
changeset 62058 1cfd5d604937
parent 61925 ab52f183f020
equal deleted inserted replaced
62057:af58628952f0 62058:1cfd5d604937
     1 (*  Title:      Pure/ML/ml_compiler_parameters.ML
     1 (*  Title:      Pure/RAW/ml_compiler_parameters.ML
     2     Author:     Makarius
     2     Author:     Makarius
     3 
     3 
     4 Additional ML compiler parameters for Poly/ML.
     4 Additional ML compiler parameters for Poly/ML.
     5 *)
     5 *)
     6 
     6