Re: [isabelle] sledgehammer info



Hi Jesus,

Am 09.02.2012 um 18:42 schrieb Jesus Aransay:

> I have this vey same question that was once solved in 2009, but which
> answers doesn't seem to work now (at least I can't do it). The
> original message (and answers) can be seen here
> https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2009-September/msg00032.html
> :
> 
> Hi,
> 
> Is there a way to get the sledgehammer to tell me exactly what input
> and options it is passing to the external ATPs?

In "sledgehammer.pdf", there's an option that's documented there, "overlord", that will do that and much more for you. I use it every day, hence the name! See the docs for details (p. 17):

http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle2011-1/doc/sledgehammer.pdf

Regards,

Jasmin
(a.k.a. the overlord)






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.