Added basic documentation for the rtl/rel9/ library, with some help from Natahlie Beavers.  This skeleton documentation reflects the organization of the online rtl manual of David Russinoff, and contains links to it.

git-svn-id: http://acl2-books.googlecode.com/svn/trunk@2531 303c5b2c-9740-0410-b014-fd8f9db7be32
add a note to build/doc.lisp linking to working-with-packages

git-svn-id: http://acl2-books.googlecode.com/svn/trunk@2532 303c5b2c-9740-0410-b014-fd8f9db7be32
Reworked witness-cp to allow more flexible use.

New versions of defwitness/definstantiate require unique names, so fix some books for this.

Localized some lemmas in witness-cp; fix books for this as well.

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

git-svn-id: http://acl2-books.googlecode.com/svn/trunk@2534 303c5b2c-9740-0410-b014-fd8f9db7be32
STD: add already-definedp option to defalist
  - Minor changes to certain hints to get already-definedp working
  - Added unit test for already-definedp in defalist-tests

VL: minor progress toward SystemVerilog expressions
  - Revised documentation about attributes
  - Switched vl-atts-p theorems to use defalist
  - Reworked defparsers to integrate better with defines
  - Started documenting vl-parse-expression, particularly attributes
  - Made attribute parsing more strict and generally more correct
  - Reworked expression unit tests to make them more reusable (for
    testing with alternate configurations, in the future)
  - Added unit tests to check attribute parsing

git-svn-id: http://acl2-books.googlecode.com/svn/trunk@2535 303c5b2c-9740-0410-b014-fd8f9db7be32
Updated basic documentation for the rtl/rel9/ library, to fix some issues including ACL2-Doc support.

git-svn-id: http://acl2-books.googlecode.com/svn/trunk@2536 303c5b2c-9740-0410-b014-fd8f9db7be32
Improve and document the logbitp-reasoning hint

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