✐‹creator "Kevin Kappelmann"› subsubsection ‹Simplification› theory Zippy_Instance_Simp imports Zippy_Instance begin ML_file‹zippy_instance_simp.ML› end