Theory Zippy_Instance_Resolves_Simp

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