Am 24.06.2011 um 20:13 schrieb Clemens Ballarin:
> While doing an 'isabelle makeall all' on my local machine, I encountered the
> error
>
> Sledgehammering...
> *** Unexpected outcome: "unknown".
> *** At command "sledgehammer" (line 26 of
> "/Users/ballarin/isabelle/hg/src/HOL/Metis_Examples/Proxies.thy")
>
>
> I guess I lack some sort of heavy equipment here. What surprises me is that
> on macbroy2 I don't have set up sledgehammer either, but I don't get this
> error.
These tests have a test to check whether you have the necessary equipment, so
this is strange. Could you tell me what
ML {* getenv "E_HOME" *}
outputs on this installation and if it's not the empty string check whether
there's an executable "eproof" script in that directory. Also, what happens if
you write
lemma "x = y ==> y = x"
sledgehammer [e, verbose]
?
Thanks,
Jasmin
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
