Normally one simply copies terms operators from a visible sample using the mouse {`(mouseleft)', `(m-(mouseright))'} perhaps even using explicit copying commands {`(c-c)', `(c-a)(c-c)', `(c-f)', `(c-a)(c-f)',}, but sometimes one simply wants to get a copy of a term onto the top of the stack so that it may be inserted with `(c-p)'.
Here are some commands that temporarily replace the top of the stack:

`(c-y)'	copies the point.
`(c-o)'	copies the operator, deleting subterms and binding variables.
`(c-a)(c-o)'	is like `(c-o)' but it also deletes parameter values.

The top of the stack is quite volatile, so for longer preservation, `(c-()' will replace the top of the stack by TWO copies of the point, and `{(m-p)(cm-p)}' will insert the second-from-the-top of the stack. You can pop the stack with `(c-))', but usually it's not worth the trouble. The stack is normally kept rather small by periodically automatically chopping off the bottom. And instead of trying to manage several stack members during cut and paste, it is clearer to simply make scratch copies in new windows with the `{scrscratch}' command which makes a scratch window containing the point value. Then just cut and paste from the scratch windows.

BUGS:

The stack is too quickly modifed when the point is on an inference step, so cut and paste must be accomplished without explicit stack manipulation commands. Commands `(c-c)', `(c-a)(c-c)' and `(m-(mouseright))' are recommended for copying an inference step on top of another. doc for proof refinement2

Two especially handy commands are `(c-u)(c-(space))', which promotes the point by deleting the parent and siblings; and `(c-u)(c-d)' which deletes the point, and if it has only one sibling, promotes that sibling by deleting the parent.

For the rest, review the individual commands with the following:

DO Review cmds for group: "Cut&Paste" IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html