Am 13.09.2013 um 09:34 schrieb Lawrence Paulson <[email protected]>: > 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 _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
