witness-cp: eliminate a beta-reduce-term name conflict

git-svn-id: http://acl2-books.googlecode.com/svn/trunk@2101 303c5b2c-9740-0410-b014-fd8f9db7be32
Clarified instructions for buildint xdoc manual.

git-svn-id: http://acl2-books.googlecode.com/svn/trunk@2103 303c5b2c-9740-0410-b014-fd8f9db7be32
fix same autolink issue, in trunk instead of jared branch

git-svn-id: http://acl2-books.googlecode.com/svn/trunk@2106 303c5b2c-9740-0410-b014-fd8f9db7be32
Incorporated into the trunk a fix from Dave Greve (which he had committed to the 6.3 branch).

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

Removed rtl/rel8 from the standard regression.  Note that rtl/rel8/lib
and rtl/rel9/support/lib3/ are much the same.  (Thanks to David
Russinoff for pointing out that rel8 is essentially part of rel9.)  In
some cases (though not in the regression), one may need to replace the
form
  (include-book "rtl/rel8/lib/top" :dir :system)
by both of the forms:
 (include-book "rtl/rel9/support/lib3/top" :dir :system)
 (include-book "rtl/rel9/arithmetic/top" :dir :system)

In tau/bounders/elementary-bounders.lisp:
Removed make-event form that turned off gag-mode, in anticipation
of impending update to acl2-devel repo that fixes this issue.


git-svn-id: http://acl2-books.googlecode.com/svn/trunk@2111 303c5b2c-9740-0410-b014-fd8f9db7be32
GL-MBE now prints a full counterexample

git-svn-id: http://acl2-books.googlecode.com/svn/trunk@2112 303c5b2c-9740-0410-b014-fd8f9db7be32
add str utility binify (like hexify)

git-svn-id: http://acl2-books.googlecode.com/svn/trunk@2113 303c5b2c-9740-0410-b014-fd8f9db7be32
gl-mbe printing bugfix

git-svn-id: http://acl2-books.googlecode.com/svn/trunk@2114 303c5b2c-9740-0410-b014-fd8f9db7be32
Very minor updates.  In XDOC, tweak to handling of leading space in <code> and
@({ ... }) sections.  In AIG, add new aig-constructors ruleset and tweak some
documentation.  In CUTIL, minor patch to defrule.




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

 - Move xdoc::save out of xdoc/top.lisp and into xdoc/save.lisp.  This
   simplifies its integration with cert.pl, and should avoid certain dependency
   problems (e.g., trying to load uncertified oslib/mkdir books).

 - Update documentation for XDOC to reflect this change, and also expand it
   with information about deploying manuals (e.g., server-supported xdoc
   manuals.)

Misc updates

 - Avoid including osets stub in cgen/library-support.lisp



git-svn-id: http://acl2-books.googlecode.com/svn/trunk@2116 303c5b2c-9740-0410-b014-fd8f9db7be32
4v-sexpr library: add SAT-based way to see if a sexpr(-list) is always Boolean
valued, via translation to FAIGs.


git-svn-id: http://acl2-books.googlecode.com/svn/trunk@2117 303c5b2c-9740-0410-b014-fd8f9db7be32
Added gl-force-true-strong and gl-force-false-strong utilities, similar to gl-force-check-strong but only checks one possibility or the other

git-svn-id: http://acl2-books.googlecode.com/svn/trunk@2118 303c5b2c-9740-0410-b014-fd8f9db7be32
gl: push default bdd-mode setting into lower-level books, so it's less likely to clobber user settings

git-svn-id: http://acl2-books.googlecode.com/svn/trunk@2119 303c5b2c-9740-0410-b014-fd8f9db7be32
Make satlink a little more permissive in parsing solver output

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

 - XDOC's fancy viewer now shows the base package for topics from packages
   other than ACL2.  (Fixes issue 100)

 - Add @(tsee ...) directive to support porting the acl2-sources documentation.




git-svn-id: http://acl2-books.googlecode.com/svn/trunk@2121 303c5b2c-9740-0410-b014-fd8f9db7be32
Mostly fix back button in xdoc viewer.

Update issue 85

This isn't a complete solution.  Pages still won't remember "subtopic expansion"
settings, and the forward-button doesn't do similar scrolling.  (Getting the
forward button to also scroll appears to be very tricky, see for instance
http://stackoverflow.com/questions/14541398).

Anyway, this is better than nothing, and at least mostly makes it work.

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

git-svn-id: http://acl2-books.googlecode.com/svn/trunk@2123 303c5b2c-9740-0410-b014-fd8f9db7be32
extremely minor cosmetic tweak for xdoc

git-svn-id: http://acl2-books.googlecode.com/svn/trunk@2124 303c5b2c-9740-0410-b014-fd8f9db7be32
GL: allow logcons terms to unify with (integer) g-number objects

git-svn-id: http://acl2-books.googlecode.com/svn/trunk@2125 303c5b2c-9740-0410-b014-fd8f9db7be32
fix xdoc.js problem that prevented firefox (but not chrome) from folloiwng links to topics.

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