ACL2-PC::TH

(macro) print the top-level hypotheses and the current subterm
Major Section:  PROOF-CHECKER-COMMANDS

Examples:
th               -- print all (top-level) hypotheses and the current
                    subterm
(th (1 3) (2 4)) -- print hypotheses 1 and 3 and governors 2 and 4,
                    and the current subterm
(th (1 3) t)     -- print hypotheses 1 and 3 and all governors, and
                    the current subterm

General Form: (th &optional hyps-indices govs-indices)

Print hypotheses and the current subterm. The printing of hypotheses (and perhaps governors) are controlled as in the hyps command; see its documentation.

Historical note: The name th is adapted from the Gypsy Verification Environment, where th abbreviates the command theorem, which says to print information on the current goal.