✐‹creator "Kevin Kappelmann"› section ‹General ML Utils› theory ML_General_Utils imports Pure begin paragraph ‹Summary› text ‹General ML utilities.› ML_file‹general_util.ML› ML_file‹either.ML› end