[isabelle-dev] Sledgehammer renaming
krauss at in.tum.de
Thu Jan 14 10:44:12 CET 2010
> 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".
> 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.
More information about the isabelle-dev