Re: [isabelle] Simplifier internal proof failure



Hi Dmitriy,

On 14/02/14 17:50, Dmitriy Traytel wrote:
> this looks like the finite_Collect simproc running havoc here again.
[...]
> For Isabelle2013-2 you can disable the simproc using
> [[simproc del: finite_Collect]]

Thanks for the hint! Turning off the simproc solves the problem both for
the minimal example and in the bigger proof I was working on.

Thanks so much,
David


________________________________

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.




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