[isabelle-dev] Total failure of sledgehammer

[Jasmin Blanchette]

Am 13.09.2013 um 09:34 schrieb Lawrence Paulson <lp15 at cam.ac.uk>:

> None of them work.

Can you reproduce it in Proof General?

As an additional test, you could try playing with options like "debug" and see if the output says anything interesting.

Just to make sure it's not MaSh-related somehow, I would also recommend you comment out "MASH=yes" in your settings file and see if this has any impact.

Another useful data point would be to know if you can run the "HOL-Metis_Examples" session. The file "Proxies.thy" contains some Sledgehammer regression tests that rely on SPASS.

Otherwise I'm running out of ideas.

Jasmin