[isabelle] sledgehammer in RC4
I just installed Isabelle2013-1-RC4 on a fresh installation of Ubuntu
13.10, using the standard "download for Linux" from the Isabelle
webpage. I built the HOL image without any problem.
Sledgehammer fails to find proofs that it found in the Isabelle2013
version. So I tried the simple example from the "First Steps" section
of "Hammering Away" from the Isabelle documentation. Only e and spass
were being called.
BTW, I fixed Z3_NON_COMMERCIAL= yes, and did not get the ususal
Isabelle warning saying to do that.
What have I forgotten?
Thanks for help,
This archive was generated by a fusion of
Pipermail (Mailman edition) and