Re: [isabelle] Interesting example of blast looping in 2016-1



I will look into this but it may take some time.
Larry

> On 10 Feb 2017, at 21:25, Makarius <makarius at sketis.net> wrote:
> 
> On 09/02/17 17:30, Lawrence Paulson wrote:
>> Your problem is not first-order and therefore lies outside the scope of blast. As I recall, there was a minor change connected with problems of that general sort. That particular example is unfortunate, but it is easily provable using other proof methods, including auto, fast and best.
>> 
>>> On 9 Feb 2017, at 04:30, Rafal Kolanski <xs at xaph.net> wrote:
>>> 
>>> âjâset w. Â j â True â set w
> 
> For the historical record, bisection produces the following result.
> 
> The first bad revision is:
> changeset:   63278:9a2377b96ffd
> user:        paulson <lp15 at cam.ac.uk>
> date:        Fri Jun 10 13:54:50 2016 +0100
> summary:     Better treatment of assumptions/goals that are simply
> Boolean variables. Also cosmetic changes.
> 
> 
> Maybe there is more to say about it.
> 
> 
> 	Makarius
> 




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