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

On 10/12/13 09:02, David Greenaway wrote:
> On 10/12/13 05:36, Makarius wrote:
>> Trying without, i.e. removing the following line
>> shows that there is no change in the success of the immediately reachable
>> universe of Isabelle + AFP examples.
>> Maybe there is a different impact on top-secret proofs that are
>> locked-up in some cellar like the Lost Ark in some Indiana Jones
>> movie, but who knows?
> Thanks for the suggestion.
> I will make the change and see how it affects all the top-secret proofs
> available in the dark cellars around here and report back.

Making this change to blast fixed the proofs that were broken by the
change in behaviour in Isabelle2013-1, and doesn't cause any new proof

Thanks for the help!



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.