✐‹creator "Kevin Kappelmann"› section ‹Instance of Zippy for Proof Search› theory Zippy_Instance imports ML_Unification.ML_Costs_Priorities Zippy_Actions_Positions Zippy_Lists_Goal_Pos_Updates Zippy_Lists_Positions_Collect Zippy_Tactics begin ML_file‹zippy_instance_base.ML› ML_file‹zippy_instance.ML› ML_file‹zippy_instance_paction.ML› ML_file‹zippy_instance_presults.ML› ML_file‹zippy_instance_tactic.ML› end