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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
