[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,
Randy




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.