		Search-engine friendly clone of the ACL2 documentation.

Defsoft-implementation

Implementation of defsoft.

Defsoft-fn: Generate the event submitted by defsoft.
Ensure-defun-sk-rule-same-funvars: Ensure that a function, if introduced by defun-sk, has an associated rewrite rule (the one generated by defun-sk that depends on exactly the same function variables that the function's matrix depends on.
Ensure-wfrel-o<: Ensure that a function, if logic-mode and recursive, has o< as well-founded relation.
Defsoft-macro-definition: Definition of the defsoft macro.