This week Robert will start a series of talks on arithmetic in ACL2.  A more
detailed description will follow shortly.