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 ...
This archive was generated by a fusion of
Pipermail (Mailman edition) and