Re: [isabelle] "blast" eliminates unrelated flex-flex pairs in Isabelle2013-1 and Isabelle2013-2.
On Tue, 10 Dec 2013, David Greenaway wrote:
It is funny that blast smashes flex-flex pairs in the first place, and
thus affects the overall goal state, not just the subgoal where it is
Indeed it is funny. I would even go so far as to say it is unexpected,
unintended and undesirable.
From the empirical data that is available, we cannot draw such a
conclusion yet. There is merely an indication that it is probably better
not to smash flex-flex here, but some uncertainty remains.
Larry might have had very good reasons to smash the flex-flex pairs in
1998. These reasons might no longer apply, or the experiments so far did
not get to the point where the difference is visible.
One needs to understand that in the old times people had much more time
thinking about problems and working on solutions. For example, the ML
compiler required many hours to work on the (then quite small) examples,
giving time for the person behind it to reconsider the present idea -- and
there was not the huge distraction of online noise of today.
This archive was generated by a fusion of
Pipermail (Mailman edition) and