PUSH 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

© 1988-99, Carnegie Mellon University.

TPS homepage