Minor VL updates and code reorganization

 - Moved some basic utilities from VL into proper homes:

    tuplep --> basic/defs
    impossible --> basic/defs
    all-equalp --> std/lists/all-equalp
    keys-boundp --> alists/fal-all-boundp

 - Improved some rules about these functions, e.g., cheapened some rules about
   all-equalp and added some good congruences for fal-all-boundp.

 - Moved worth-hashing from misc/hons-help into std/alists.

 - Added a systest for basic port handling.

 - The pretty-printer now treats VL_PORT_IMPLICIT in a special way.  This
   should generally produce slightly nicer pretty printed output, and is
   perhaps important for proper support of SystemVerilog ANSI-style module
   declarations.

   (Some details: in non-ANSI style module declarations, Verilog weirdly allows
   ports to be subsequently declared as nets, e.g., you can write ``input a;
   wire a;``.  When no such net declaration is made, VL creates one and marks
   it with the VL_PORT_IMPLICIT attribute.  Previously these attributes weren't
   used for anything.  But now, toward supporting ANSI-style port lists where
   it isn't legal to have a subsequent net declaration of a port, the
   pretty-printer will just omit any nets that are marked as VL_PORT_IMPLICIT.

 - Various trivial documentation fixes and updates to other books due to
   std changes.

git-svn-id: http://acl2-books.googlecode.com/svn/trunk@2955 303c5b2c-9740-0410-b014-fd8f9db7be32
Added documentation for the recently-added SIMP utility (defined in
misc/simp.lisp).

Changed parents of topics PSO, PSO!, PSOF, and PSOG to PROVER-OUTPUT.

Added documentation for FORMULA.

Updated :doc note-7-0 in system/doc/acl2-doc.lisp:

 (GCL only) Modified how home directory is calculated.  Thanks to Camm
 Maguire for help in making this change.

Updated ``make everything'' with help from Jared, as explained in this
new paragraph from :doc note-7-0-books (which was also edited to
replace remaining references to 6.6 by 7.0).

  The implementation of ``make everything'' has been cleaned up. In
  particular, it no longer sets USE_QUICKLISP=1, which must now be
  provided explicitly in order for the command above to build the
  ACL2+Books Manual.

Made a few comment mods.

In projects/milawa/ACL2/acl2-hacks/half-translate.lisp, replaced the
definition of tuplep with definition from std/basic/defs.lisp (by
including that book), to avoid redefinition error encountered when
attempting to certify projects/milawa/ACL2/acl2-hacks/defun.lisp.


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

This is a fairly aggressive attmept to reorganize many ACL2 topics, mostly from
acl2-built-ins, into related groups such as alists, arrays, characters, errors,
numbers, packages, etc.

This reorganization is done in doc/top.lisp:fix-the-hierarchy, so it should
only affect the web-based manual, and it should be easy to undo if people do
not think it is progress.

This is very much a half-assed first draft, and there are a lot of things that
obviously need a lot of work.  For instance, it's probably not sensible to have
all of these things directly underneath ACL2.  I'd appreciate feedback on the
general idea and how to improve upon it.

Also: hack to improve strings/pretty-program certification time.

git-svn-id: http://acl2-books.googlecode.com/svn/trunk@2957 303c5b2c-9740-0410-b014-fd8f9db7be32
Made changes to avoid exhausting the available space when using GCL
2.6.8:

  workshops/2009/sumners/support/kas.acl2 (for certifying kas.lisp)
  centaur/vl/cert.acl2 (for certifying centaur/vl/parsetree.lisp)


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