Re: [Hol-developers] theorem restoration

[Joe H. <je...@he...>]

On Fri, 31 May 2002, Konrad Slind wrote:

> Re: strip_X, spine_X, rspine_X, lspine_X, or whatever these  things are
> called: I'd really prefer something like "flatten_X instead of strip_X,
> and strip_X instead of spine_X. But making the transition looks too
> complicated!

With my 'starting HOL from scratch' hat on, I'd have to agree that
these are much more intuitive names.

Returning to the real world...

Joe