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
>> http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2013-2/src/Provers/blast.ML#l1261
>> 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
breakage.

Thanks for the help!

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.