[isabelle] Two configuration questions



Dear all,

I have some trouble configuring a fresh Isabelle2013-2/jedit installation:

1. It seems that sledgehammer only invokes "e" and "spass". How can I configure it to invoke more solvers (e.g. those that Isabelle2011 invoked by default)? It would be best if this is a persistent configuration setting, so that I don't have to repeat it every time I launch Isabelle or sledgehammer.

2. Auto completion used to show a drop-down box with the sigma character when I typed "sig". Similarly, it used to show an existential quantifier when I typed "exists". This does not work anymore. How can I turn it on again?

Many thanks,
Stephan




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