Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Question about Sledgehammer

Email Gateway (Aug 19 2022 at 11:29):

From: Antoine Grospellier <antoine.grospellier@ens-lyon.fr>
Hello everybody,

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

Thanks,
Antoine Grospellier.

Email Gateway (Aug 19 2022 at 11:30):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
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

Last updated: Apr 19 2024 at 08:19 UTC