Merge pull request #312 from acl2/testing

Bring in changes from testing
Small toothbrush enhancements, mainly providing support for ACL2(p).
Eliminated compiler warning introduced earlier this morning.  Synched doc.lisp.
Merge branch 'master' into testing