From: Joe H. <je...@he...> - 2002-05-31 20:54:07
|
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 |