[isabelle-dev] Vampire

Makarius makarius at sketis.net
Wed Jul 4 13:29:48 CEST 2018


On 04/07/18 12:11, Blanchette, J.C. wrote:
> 
> I just copied old code I inherited from Sascha Böhm and his Vampire noncommercial.

I only vaguely remember when we introduced the original non-commercial
settings variable for Z3, even with some insider joke about Microsoft:
changing the value required a reboot of the Isabelle application. Later
it became a system option for change at run-time, not boot-time.

I don't remember the reason for its "tristate logic", with "unknown" as
default.

If you make it a plain bool with false as default, users can just click
on a checkbox in Isabelle/jEdit Plugin options.


	Makarius




More information about the isabelle-dev mailing list