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

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.


	Makarius




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