LEFT-hand version recommended.

Stores the object to the library, perhaps checking it, and perhaps storing a copy to disk.

Kind	Post?	Check?	DiskSave?(if enabled)
ABS	y	y	y
DISP	y	y	y
LAT	y	y	y
RULE	y	y	y
COM	y	n	y
ML	y	n	y
GoalBox	y	n	n
RuleBox	y	n	n

Simply posting a thm goal or rule will leave the subproofs unaffected as long as the unconditional expansion results in the same term.
You have to use `(c-z)' to substantially change the goal of a theorem with a non-empty proof, or to effect the refinement of a rule.
You can store a "proof term" to a THM object with `(c-a)(c-v)'.

Some posting primitives:
(m-x)restore will restore to the last posted value, or ot the value the object had when the window was opened.
(m-x)reset will reset to the last posted or (m-x)restore'd value. IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html