Add gl-and-use-example

git-svn-id: http://acl2-books.googlecode.com/svn/trunk@2585 303c5b2c-9740-0410-b014-fd8f9db7be32
Clarifying some documentation in accumulated-persistence.

git-svn-id: http://acl2-books.googlecode.com/svn/trunk@2586 303c5b2c-9740-0410-b014-fd8f9db7be32
Updating :doc for acl2-devel revision 1258 -- Quoting :doc note-6-5:

  When forcing (see [force]) is applied, we now always see the
  appropriate [executable-counterpart] [rune],
  (:executable-counterpart force), in the proof output and summary;
  this hadn't previously been the case. Thanks to Robert Krug for
  bringing this issue to our attention.


git-svn-id: http://acl2-books.googlecode.com/svn/trunk@2587 303c5b2c-9740-0410-b014-fd8f9db7be32
certlib: fix a problem with "cert.pl -p top.lsp" style usage

git-svn-id: http://acl2-books.googlecode.com/svn/trunk@2588 303c5b2c-9740-0410-b014-fd8f9db7be32
Fixing up accumulated persistence doc topic

git-svn-id: http://acl2-books.googlecode.com/svn/trunk@2589 303c5b2c-9740-0410-b014-fd8f9db7be32
Clarified dependence of tau on enable/disable status of executable-counterpart runes, thanks to discussion with Robert Krug and J.

git-svn-id: http://acl2-books.googlecode.com/svn/trunk@2590 303c5b2c-9740-0410-b014-fd8f9db7be32
Add hons-only tag to new demos/gl-and-use-example book

git-svn-id: http://acl2-books.googlecode.com/svn/trunk@2591 303c5b2c-9740-0410-b014-fd8f9db7be32
localize a rule in aignet

git-svn-id: http://acl2-books.googlecode.com/svn/trunk@2592 303c5b2c-9740-0410-b014-fd8f9db7be32
1. replaced defxdoc by defdoc in with-timeout 2. fixed a bug arising in a corner case: combination of programp and verify-guards t is not allowed in an attachable function

git-svn-id: http://acl2-books.googlecode.com/svn/trunk@2593 303c5b2c-9740-0410-b014-fd8f9db7be32
deleted irrelevant ld in portcullis. Sedan code synced r1094

git-svn-id: http://acl2-books.googlecode.com/svn/trunk@2594 303c5b2c-9740-0410-b014-fd8f9db7be32
Added demos/knuth-bendix-problem-1.lisp and updated documentation accordingly.

git-svn-id: http://acl2-books.googlecode.com/svn/trunk@2595 303c5b2c-9740-0410-b014-fd8f9db7be32
Fixing defrule to accept prepwork-like fields 
Fixes 151

git-svn-id: http://acl2-books.googlecode.com/svn/trunk@2596 303c5b2c-9740-0410-b014-fd8f9db7be32
added a guard-checking t wrapper to all-xdoc-topics to get :doc to work in sessions with set-guard-checking set to :none (some ACL2s modes default to it)

git-svn-id: http://acl2-books.googlecode.com/svn/trunk@2597 303c5b2c-9740-0410-b014-fd8f9db7be32
Major VL update and other supporting changes

Supporting changes to other libraries:

  - Esim: replaced the remaining defdoc documentation with defxdoc
    documentation

  - Defmvtypes: smarter handling of force, eliminated unnecessary
    dependency on defalist

  - Moved std/util testing code into a new std/util/tests directory

  - Factor out defaggregate-style emulation for defrecs, out of
    tools/lint and into std/defaggrify-defrec.lisp, and added some
    basic tests.

  - Tweaks for the documentation generated by DEFINES, which still
    isn't great, but at least no longer results in a lot of top-level
    topics.

  - Other updates, e.g., to centaur/regression, tutorial, stv2c,
    etc., to cope with the VL changes described below.

VL changes:

A vl-design-p is a new aggregate.  It has a module list as one of its
components.  It will eventually also have other top-level SystemVerilog design
elements such as packages, interfaces, etc.

  - VL's loader now produces a design instead of a module list.

  - All VL transforms now take and (unconditionally!) return vl-design-p
    objects instead of vl-modulelist-p objects.

  - The vl-translation-p objects (produced by, e.g., vl-simplify and
    defmodules) now contain good/bad/orig vl-design-p objects instead of module
    lists.

Lots of various cleanups and enhancements:

  - Almost all VL transforms and checkers have been modernized to take
    advantage of DEFINE, DEFINES, WARN, FATAL, SET-DEFAULT-PARENTS, etc.  The
    code is somewhat shorter, and documentation is considerably improved.

  - The vl-propagate-errors code has been extended to designs (sort of) and
    simplified so that it no longer requires uniqueness of modulelist names.
    This mostly eliminates the need to worry about the module names returned
    by transforms, so we no longer prove that most transforms preserve their
    input module names.

  - The interface to unparameterization is now considerably simpler, with no
    more complex guards about good parameter lists, etc.

  - The vl-simplify code no longer needs to be split into separate functions,
    thanks to the above changes and thanks to help from Sol in developing a
    clever meta rule to avoid quadratic blowups due to vl-propagate-errors;
    see mlib/design-meta.lisp and vl-design-propagate-errors* in top.lisp.

  - Remove old standalone use-set tool.

Various additional fixes for documentation and the centaur tutorial

git-svn-id: http://acl2-books.googlecode.com/svn/trunk@2598 303c5b2c-9740-0410-b014-fd8f9db7be32
Fixing (purportedly) latest defrule changes to work with cert.pl.  I spot checked the generated Makefile-tmp file that my project has, and it looks like the dependencies are being found.  Fixes issue 151

git-svn-id: http://acl2-books.googlecode.com/svn/trunk@2599 303c5b2c-9740-0410-b014-fd8f9db7be32
added new symbols to be exported: range _

git-svn-id: http://acl2-books.googlecode.com/svn/trunk@2601 303c5b2c-9740-0410-b014-fd8f9db7be32
certlib: fix for missing files so we don't incorrectly complain about dependency loops

git-svn-id: http://acl2-books.googlecode.com/svn/trunk@2602 303c5b2c-9740-0410-b014-fd8f9db7be32
Tweak defaggregate b* binder guts so they can be used with different accessor names

git-svn-id: http://acl2-books.googlecode.com/svn/trunk@2603 303c5b2c-9740-0410-b014-fd8f9db7be32
Small updates in consultation with Cuong.

git-svn-id: http://acl2-books.googlecode.com/svn/trunk@2605 303c5b2c-9740-0410-b014-fd8f9db7be32
Initial commit of tool, written by Nathan and me (Matt), for attempting to remove unnecessary hypotheses from an IMPLIES formula of a DEFTHM form.

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