PUSH : MEXPRPUSH is a top-level command.
Start a new top level. This command is almost useless,
except from within a prompt (e.g. one can type PUSH in the middle
of converting an etree to a ND proof interactively, call SCRIBEPROOF,
and then type POP to return to the conversion).
The command format for PUSH is:
TPS documentation homepage