✐‹creator "Kevin Kappelmann"› section ‹ML-Normalisations› theory ML_Normalisations imports ML_Conversion_Utils begin paragraph ‹Summary› text ‹Normalisation functions for terms, types, and theorems.› ML_file‹term_normalisation.ML› ML_file‹envir_normalisation.ML› end