Filtering...

real-listp

books/arithmetic/real-listp
other
(in-package "ACL2")