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



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).

  -- Lars


Attachment: signature.asc
Description: OpenPGP digital signature



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.