		Search-engine friendly clone of the ACL2 documentation.

Defaults-table

Set-default-input-old-if-new-enable

Set the default :old-if-new-enable input of APT transformations.

Some APT transformations include an :old-if-new-enable input that specifies whether to enable the generated theorem asserting that the old function is implied by the new function.

This macro sets an entry in the APT defaults table that provides the default value of the :old-if-new-enable input. It must be a boolean.

The initial value of this default is nil.

Macro: set-default-input-old-if-new-enable

(defmacro set-default-input-old-if-new-enable (bool)
  (declare (xargs :guard (booleanp bool)))
  (cons 'table
        (cons *defaults-table-name*
              (cons ':old-if-new-enable
                    (cons bool 'nil)))))