[isabelle-dev] Sledgehammer renaming

[Jasmin Blanchette]

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