Split out ACL2(r) compatible stuff in arithmetic-3/extra/ext.lisp into a new book, to try to simplify the build process.

git-svn-id: http://acl2-books.googlecode.com/svn/trunk@2384 303c5b2c-9740-0410-b014-fd8f9db7be32
Fix up issues with ext.lisp in ACL2(r) build

git-svn-id: http://acl2-books.googlecode.com/svn/trunk@2385 303c5b2c-9740-0410-b014-fd8f9db7be32
Adding some compare and contrast for GL vs Rewriting.  Thanks Sol for providing the basis for this explanation

git-svn-id: http://acl2-books.googlecode.com/svn/trunk@2386 303c5b2c-9740-0410-b014-fd8f9db7be32
Adding the GL version of the boothmultiplier decomposition lemma back into the tutorial, since it's instructive.

git-svn-id: http://acl2-books.googlecode.com/svn/trunk@2387 303c5b2c-9740-0410-b014-fd8f9db7be32
fix up temp theorem names in arithmetic-3 (fixes issue 126)

git-svn-id: http://acl2-books.googlecode.com/svn/trunk@2388 303c5b2c-9740-0410-b014-fd8f9db7be32
Build system documentation updates

git-svn-id: http://acl2-books.googlecode.com/svn/trunk@2389 303c5b2c-9740-0410-b014-fd8f9db7be32

Installed improved comment from J in pseudo-good-worldp.lisp.

Improved documentation about copyrights and made other miscellaneous
improvements to books/system/doc/acl2-doc.lisp.  In particular, fixed
use of a package prefix in new books-certification topic that was
breaking the text-rendered manual (for :doc and ACL2-Doc).


git-svn-id: http://acl2-books.googlecode.com/svn/trunk@2390 303c5b2c-9740-0410-b014-fd8f9db7be32