document new delayredux options

git-svn-id: http://acl2-books.googlecode.com/svn/trunk@2966 303c5b2c-9740-0410-b014-fd8f9db7be32
vl: gate-elim transform: map from gates to modules using an alist passed in to the transform, rather than a hardcoded function

git-svn-id: http://acl2-books.googlecode.com/svn/trunk@2967 303c5b2c-9740-0410-b014-fd8f9db7be32
vl: start of interface parsing

git-svn-id: http://acl2-books.googlecode.com/svn/trunk@2968 303c5b2c-9740-0410-b014-fd8f9db7be32
Updated ACL2 system documentation for this (quoting :doc note-7-0):

  When the [ld-evisc-tuple] is non-nil, the utilities :[pe], :[pc], and
  :[pbt!] now abbreviate their output accordingly. See
  [set-evisc-tuple]. Thanks to David Rager for bringing the need for
  this change to our attention.


git-svn-id: http://acl2-books.googlecode.com/svn/trunk@2969 303c5b2c-9740-0410-b014-fd8f9db7be32
Disable part-install-width-low in centaur/bitops/part-install

git-svn-id: http://acl2-books.googlecode.com/svn/trunk@2970 303c5b2c-9740-0410-b014-fd8f9db7be32
Added this to :doc note-7-0 to reflect acl2-devel update:

  The heuristics have changed for guessing the :typed-term field for a
  :[type-prescription] rule when that field is not explicitly
  specified. Specifically, consider the case that the conclusion of
  the rule is a function call (p u) for some term u, such that there
  is an enabled [compound-recognizer] rule for p. Formerly, the
  :typed-term was u in this case. Now, it must be the case that the
  most recent enabled such [compound-recognizer] rule is `strong', in
  the following sense: if ts1 is the [type-set] implied by assuming
  the conclusion true and if ts2 is the [type-set] implied by
  assuming the conclusion false, then ts1 and ts2 are complementary.
  Thanks to Jared Davis for an email that prompted us to make this
  change.


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