[isabelle-dev] Sledgehammer renaming

[Alexander Krauss]

Makarius wrote:
> On Wed, 13 Jan 2010, Jasmin Blanchette wrote:
>> 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".

Makarius wrote:
> Although the "ATP" manager can technically manage almost everything, 

Actually having such an "everything_manager", which deals with all the 
trouble of running things asynchronously would be an important thing. At 
some point I will also need this functionality, for connecting to 
external termination provers.

Maybe a UI architecture which is inherenetly asynchronous will provide 
this anyway and be even more general... But so far, atp_manager is the 
best we have, and it would be nice if it could be used for other tools, too.

Alex