Re: [isabelle] Bug in Sledgehammer / cvc4

Hi Bohua,

Using 2015/Windows with try methods I get with cvc4:

using Max_ge not_le by blast

Without try methods: by (metis Max_ge leD)



On Mon, Jun 22, 2015 at 4:57 PM, Bohua Zhan <bzhan at> wrote:

> When I tried sledgehammer on the following theorem:
> theorem Max_ge': "finite A â x > Max A â Â(x â A)"
> The cvc4 output is:
> Try this: using leD by auto (6 ms).
> However, the command does not work. It probably should be
> using Max_ge leD by auto
> Best,
> Bohua

Alfio Ricardo Martini
PhD in Computer Science (TU Berlin)
Associate Professor at Faculty of Informatics (PUCRS)
Av. Ipiranga, 6681 - PrÃdio 32 - Faculdade de InformÃtica
90619-900 -Porto Alegre - RS - Brasil

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