[isabelle] trouble with sledgehammer/ProofGeneral in Isabelle2013



Hi,

I just switched to Isabelle2013.  If sledgehammer returns a proof "try
...",  I see this proof message in the response buffer for second,
then "Process isabelle exited abnormally with code 133, shutting down
scripting.

I'm using Isabelle2013 64 bit, Kubuntu, ProofGeneral 4.1, emacs
23.4.1.  Same problem with PG 4.2 and with emacs 24.

Works with Isabelle2012 package; also works in Isabelle2012 using PG
4.2 and emacs 24.

Other users must have used sledgehammer in ProofGeneral, so I must be
doing something wrong, but what?

Thanks for any help,
Randy




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