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


When updating one of our branches to 2016-1 I came across blast looping
on this subgoal when it did not do so previously:

âjâset w. Â j â True â set w

Interestingly, blast is OK with this one:

âjâset w. Â j = True â True â set w

and also

âjâset w. j = False â True â set w

Any ideas what changed to cause this? In this case I switched over to
fastforce due to being in a hurry, but it would be useful to understand
for future reference.


Rafal Kolanski

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