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