Set-default-input-old-if-new-name
Set the default :old-if-new-name input of APT transformations.
Some APT transformations include an :old-if-new-name input
that specifies the name of the generated theorem
asserting that the old function is implied by the new function.
When this input is a symbol that is a valid theorem name,
it is used as the theorem name.
When this input is a keyword (which is never a valid theorem name),
the theorem name is the concatenation of
the old function name, the keyword, and the new function name,
e.g. f-if-g if
f is the old function name,
g is the new function name,
and :-if- is the keyword passed as the :old-if-new-name input.
Thus, the keyword specifies a separator
between old and new function names.
The concatenated symbol is in the same package as the new function name.
This macro sets an entry in the APT defaults table
that provides the default value of the :old-if-new-name input.
It must be a keyword, which is used as a separator as described above.
It would not make sense to have a complete theorem name as default.
The initial value of this default is :-if-.
Macro: set-default-input-old-if-new-name
(defmacro set-default-input-old-if-new-name (kwd)
(declare (xargs :guard (keywordp kwd)))
(cons 'table
(cons *defaults-table-name*
(cons ':old-if-new-name
(cons kwd 'nil)))))