		Search-engine friendly clone of the ACL2 documentation.

ACL2-pc::th

(macro) print the top-level hypotheses and the current subterm

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 ACL2-pc::hyps.

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.