[isabelle-dev] Sledgehammer renaming
jasmin.blanchette at gmail.com
Wed Jan 13 14:55:22 CET 2010
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?
More information about the isabelle-dev