Please email suggestions for improvements to the ACL2 developers or to
ewsmith@stanford.edu.

Use user/ at your own risk!  The user/ directory is an attempt to pull out some useful rules which were in
support/ but not in lib/.  However, like support/, user/ is kind of a mess. There wasn't time to think through
all of the rules we added to user/, but it seemed better to create it than to do nothing.  Someday, we'd like
to think through user/ and create a really nice set of books.

Many or most (or all) of the user/ books were derived from books with the same names in support/.  More
extensive comments can be found in the latter, along with extra lemmas in some cases. The reader is welcomed
to compare correponding user/ and support/ books to see what is missing from user/, and to suggest
improvements.

BOZO Currently, there may be a problem with user/: Eventually we want to make it good enough to be a
replacement for lib/, but right now, it lacks some rules from lib/ (not all the books we plan to put in user/
have been created).  So one should include books from lib/ and the optional user/ books.  But this means that
a rule disabled in lib/ but intentionally enabled in user/ will still be disabled for that person.  We could
add explicit enables in user/ (and include user/ after including lib/) as we discover such lemmas.

For rules about functions not mentioned in user/ here but which arise from opening up functions dealt with in
user/ (e.g., binary-logand which arises from opening binary-land), see the appropriate books in support/ e.g.,
support/binary-logand).