✐‹creator "Kevin Kappelmann"› subsection ‹Prover with Resolution and Simplification› theory Zippy_Instance_Resolves_Simp imports Extended_Simp_Data Zippy_Instance_Resolve begin paragraph ‹Summary› text ‹Basic ingredients for a prover supporting resolution and simplification based on Zippy.› setup‹Context.theory_map ML_Gen.ground_zipper_types› ML_file‹zippy_instance_resolves_simp.ML› setup‹Context.theory_map ML_Gen.reset_zipper_types› end