On 18/09/2022 10:21, Lawrence Paulson wrote: > Wow. What is MLton used for? It is occasionally used with SML codegeneration, to produce a high-end executable. AFP/59b24f0e98b1 has the following occurrences of ISABELLE_MLTON: Buchi_Complementation Native_Word PAC_Checker Makarius