Re: [isabelle] Two configuration questions
I'm afraid this does not solve my problem. The shell variables help to locate local (as opposed to remove) solvers, but I want to invoke remote ones plus the standard ones that come with Isabelle2013-2.
From: Buday Gergely [gbuday at karolyrobert.hu]
Sent: Monday, February 10, 2014 4:13 PM
To: Van Staden Stephan; cl-isabelle-users at lists.cam.ac.uk
Subject: RE: Two configuration questions
gives you details on how to set the necessary shell variables. If on Windows, you should start the batch file that gives you a cygwin prompt and then go ahead. Read the section 2 Installation.
From: cl-isabelle-users-bounces at lists.cam.ac.uk [cl-isabelle-users-bounces at lists.cam.ac.uk] On Behalf Of Van Staden Stephan [stephan.vanstaden at inf.ethz.ch]
Sent: Monday, February 10, 2014 3:22 PM
To: cl-isabelle-users at lists.cam.ac.uk
Subject: [isabelle] Two configuration questions
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?
This archive was generated by a fusion of
Pipermail (Mailman edition) and