PROPOSITIONAL : TACTICPROPOSITIONAL is a tactic.
As defined for use NAT-DED:
(ORELSE MAKE-ROOM (TRY (REPEAT PROP-PRIM))
(THEN INDIRECT-TAC PROPOSITIONAL)))
First tries PROP-PRIM repeatedly. If any goals remain, what work
was done is thrown away, indirect proof is applied, and PROPOSITIONAL
is called recursively on the new goal.
TPS documentation homepage