Re: [isabelle] Simplifier internal proof failure
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,
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