Major Section: MISCELLANEOUS
...the word ``command'' usually refers to a top-level form whose evaluation produces a new logical world.
Typical commands are: (defun foo (x) (cons x x)) (defthm consp-foo (consp (foo x))) (defrec pair (hd . tl) nil)The first two forms are examples of commands that are in fact primitive events. See events.
Defrec, on the other hand, is a
macro that expands into a progn of several primitive events. In
general, a world extending command generates one or more events.
Both events and commands leave landmarks on the world that enable us
to determine how the given world was created from the previous one.
Most of your interactions will occur at the command level, i.e., you
type commands, you print previous commands, and you undo back
through commands. Commands are denoted by command descriptors.
See command-descriptor.