Major Section: ACL2-BUILT-INS
List* is the Common Lisp macro for building a list of objects from
given elements and a tail. For example, (list* 5 6 '(7 8 9)) equals
the list '(5 6 7 8 9). Also see list.
List* is a Common Lisp function. See any Common Lisp
documentation for more information.
