Re: [isabelle] "blast" eliminates unrelated flex-flex pairs in Isabelle2013-1 and Isabelle2013-2.



On 10/12/13 23:42, Makarius wrote:
>    * Is there any performance impact on changing the behaviour?  So far
>      the success or failure was not affected, but there were no
>      measurements of timing so far.

As a single data point, I am not seeing any performance change on my
proof scripts. (A slight performance improvement after the change, but
well within the margin of noise.)

Cheers,
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.