PROPOSITIONAL : TACTIC

PROPOSITIONAL is a tactic.
As defined for use NAT-DED:
(REPEAT
(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


© 1988-99, Carnegie Mellon University.

TPS homepage