		Search-engine friendly clone of the ACL2 documentation.

Install-not-normalized$

Install the non-normalized definition of a function, ensuring that the name of the theorem will not cause a conflict.

This utility is an event which, when evaluated successfully, installs the event generated by install-not-normalized-event. See install-not-normalized-event.

This is related to install-not-normalized.

Macro: install-not-normalized$

(defmacro install-not-normalized$ (fn &key allp names-to-avoid)
 (cons
      'make-event
      (cons (cons 'install-not-normalized$-fn
                  (cons (cons 'quote (cons fn 'nil))
                        (cons allp (cons names-to-avoid '(state)))))
            'nil)))