eql
Major Section: PROGRAMMING
(remove x l) is l if x is not a member of l, else is the
result of removing all occurrences of x from l.
The guard for (remove x l) requires l to be a true list and
moreover, either x is eqlablep or all elements of l are
eqlablep.
Remove is a Common Lisp function. See any Common Lisp
documentation for more information. Note that we do not allow
keyword arguments (such as test) in ACL2 functions, in
particular, in remove.
Also see remove1, see remove-equal, and see remove-eq.