Slightly expand doc of APPLY-TERM and APPLY-TERM*.

Mention that these two utilities extend CONS-TERM and CONS-TERM* to lambda expressions.
acl2 · Oct 14, 2017 · d8339ae · d8339ae
1 parent a7846ac
commit d8339ae
Showing 1 changed file with 6 additions and 0 deletions.
diff --git a/books/kestrel/utilities/terms.lisp b/books/kestrel/utilities/terms.lisp
@@ -112,6 +112,9 @@
   :long
   "<p>
    If a lambda expression is applied, a beta reduction is performed.
+   </p>
+   <p>
+   This utility extends @(tsee cons-term) to lambda expressions.
    </p>"
   (cond ((symbolp fn) (cons-term fn terms))
         (t (subcor-var (lambda-formals fn) terms (lambda-body fn))))
@@ -126,6 +129,9 @@
   "<p>
    If a lambda expression is applied, a beta reduction is performed.
    </p>
+   <p>
+   This utility extends @(tsee cons-term*) to lambda expressions.
+   </p>
    @(def apply-term*)"
   (defmacro apply-term* (fn &rest terms)
     `(apply-term ,fn (list ,@terms))))