APPLY-RRULE-1 : WFFOPAPPLY-RRULE-1 is a wff operation.
Apply a rewrite rule (active or inactive) to the
current edwff. If the rule is bidirectional, you will be
prompted about which direction to apply it in.
The calling scheme for APPLY-RRULE-1 is:
(APPLY-RRULE-1 GWFF RULE)
The result is of type GWFF.
The arguments have the following meaning:
GWFF : gwff before rewriting
RULE : name of rule
TPS documentation homepage