Theory ML_Normalisations

✐‹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