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

On 12 Dec 2013, at 1:22 am, Lars Noschinski <noschinl at> wrote:

> On 11.12.2013 14:58, Makarius wrote:
>> From this I guess that your change Isabelle/93a84eb6c522 from 02-Jan-1998
>> no longer conforms to what you would do today.  Although it is hard to
>> tell precisely, since flex-flex pair are extremely rare, and defining an
>> intended meaning operates almost at 0 entropy.
> I guess the rarity of flex-flex pairs depends on the kind of proofs you
> do. I recently wrote a VCG for program refinement, consisting mainly of
> a large set of introduction rules. I remember seeing flex-flex pairs
> quite often for the intermediate results (although the usually would
> disappear when the VCG successfully completed).

Yes, that’s very similar to the kinds of proofs we have.

flex-flex pairs are still rare in our proofs, but they do pop up occasionally.



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.