Re: [isabelle] Question about Sledgehammer



Hi Antoine,

According to the tutorial on sledgehammer (end of section 7.1) at
http://isabelle.in.tum.de/dist/Isabelle2013/doc/sledgehammer.pdf
you can tell sledgehammer to output the files in $ISABELLE_HOME_USER (this usually is ~/.isabelle/Isabelle2013 for Isabelle2013) by passing the overlord option:

sledgehammer [overlord]

Best,
Andreas

On 01/07/13 14:34, Antoine Grospellier wrote:
Hello everybody,

Is it possible to see what sledgehammer sends to the automatic provers?

Thanks,
Antoine Grospellier.






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