ACL2 is both a programming language in which you can model computer
 systems and a tool to help you prove properties of those models.
 .
 This package contains utilities and libraries to access ACL2 via an
 infix notation similar to that used in many non-lisp programming
 languages.