[isabelle-dev] sledgehammer

[Makarius]

On Mon, 2 Sep 2013, Tobias Nipkow wrote:

> But you are right, this could lead to complications in the 
> implementation.

At the moment we can ignore questions about "implementation", it is done 
quite differently anyway from what one might expect.  The sledgehammer 
dialog box appears to look like a conventional GUI, but it is going 
through several layers of concepts behind the scenes.

If there is something fundamentally wrong there, it cannot be changed 
easily.  On the other hand, various fine points might be just a matter of 
some fine tuning of the use of these concepts.

I will come back to this thread a bit later, when more impressions have 
been collected.


 	Makarius