✐‹creator "Kevin Kappelmann"› subsection ‹Classical Reasoner› theory Zippy_Instance_Classical imports HOL.HOL Zippy_Instance begin ML_file‹zippy_instance_classical.ML› end