Re: [isabelle] provers used by sledgehammer



On Fri, 20 Jul 2012, Jasmin Blanchette wrote:

If you change it through the good old Proof General settings, I think it will do the right thing and remember it across sessions. Otherwise, no: That's what "sledgehammer_params" is for, and it would be tedious to emulate its functionality in "etc/settings" (e.g. to change the default timeout or whatever else...).

Note again that Isabelle Proof General is umaintained since October 2011, so it has reached End-of-Life unless someone else stands forward to continue its maintenance. (Pretty soon I will stop reminding people of this, and then it is really dead.)


Concerning the current Isabelle/Scala and Prover IDE infrastructure, there is still no persistent preferences mechanisms, but I am working on it.

Righ now one can imitate what Proof General did here by hand:

  ML {* Sledgehammer_Isar.provers := "e spass vampire" *}


	Makarius





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