Re: [isabelle] Isabelle2016-RC0: cvc4 crashing



I will see what I can do, but it is not deterministically repeatable,
and I usually just invoke sledgehammer by typing "try" or "try0".

						- Gene Stark

On 01/14/2016 02:36 PM, Jasmin Blanchette wrote:
> 
>> On 14.01.2016, at 19:49, Eugene W. Stark <isabelle-users at starkeffect.com> wrote:
>>
>> Where do I put this magic incantation?
> 
> Right after the proof goal or lemma you are trying to prove, directly in the text editor (at the point where you would normally invoke Sledgehammer through its dedicated panel). E.g.
> 
>     lemma "x = x"
>     sledgehammer [overlord]
> 
> Jasmin
> 
> 





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