INSTANTIATE-DEFN : WFFOPINSTANTIATE-DEFN is a wff operation.
Instantiate all occurrences of an abbreviation.
The occurrences will be lambda-contracted, but not lambda-normalized.
The calling scheme for INSTANTIATE-DEFN is:
(INSTANTIATE-DEFN GABBR INWFF)
The result is of type GWFF.
The arguments have the following meaning:
GABBR : abbrev
INWFF : inwff
TPS documentation homepage