Re: [isabelle] sledgehammer in RC4
Am 11.11.2013 um 12:06 schrieb Makarius <makarius at sketis.net>:
> On Sat, 9 Nov 2013, Randy Pollack wrote:
>> BTW, I fixed Z3_NON_COMMERCIAL= yes, and did not get the ususal
>> Isabelle warning saying to do that.
>> What have I forgotten?
> I don't understand the "fixed Z3_NON_COMMERCIAL" part. What was broken here?
No. The message did not show up because only two provers were run (E and SPASS). That's perfectly normal. The message is shown only if users attempt to run Z3.
This archive was generated by a fusion of
Pipermail (Mailman edition) and