Hi, Tobias asked me to look at Sledgehammer and see if it would be possible to improve the relevance filter and the proof reconstruction to get a better success rate. As a first step towards that, I was thinking of refactoring the Sledgehammer code. In particular:
1. Put all the Sledgehammer files in "HOL/Tools/Sledgehammer" (and remove the "res_" prefixes and give clearer names, e.g. "fact_filter.ML" instead of "res_atp.ML"). 2. Generalize "atp_manager.ML" so that it can manage arbitrary "assistants", which are tools that take a goal and produce a message -- not just ATPs -- and rename it "HOL/Tools/assistant.ML". Does anybody have objections/comments? Jasmin