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



On Tue, 10 Dec 2013, Lawrence Paulson wrote:

I’m puzzled about this. I thought the issue was that flex-flex constraints were suddenly being smashed now, when they were not before. And I would certainly not have wanted every blast call to smash all flex-flex constraints, because this can lose completeness.

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.

Anyway, after heating my office with more CPU power (running Isabelle + AFP + IsaFoR a few times), I have the impression that there is nothing to see on this thread, and we can just move on. This means we can probably remove the extra clean-up step from blast in coming Isabelle versions.

Further explanations when the current build has terminated ...


	Makarius


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