Re: [isabelle] Two configuration questions



Hi Buday,

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.

Stephan

________________________________________
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

Hi Stephan,

for 1,

http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle2013-2/doc/sledgehammer.pdf

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.

- Gergely
________________________________________
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

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.