pete: updated ordinals

git-svn-id: http://acl2-books.googlecode.com/svn/trunk@2357 303c5b2c-9740-0410-b014-fd8f9db7be32
pete: updated natp-posp

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

In support of the following ACL2 change (about to be checked into
acl2-devel as svn revision 1188), added book
demos/patterned-congruences.lisp and modified a few other books
slightly.  Quoting :doc note-6-4:

  The class of [congruence] rules has been broadened considerably, so
  that one can restrict to patterns. For example, a congruence rule
  can now state that an equivalence is maintained for the term
  (mv-nth 1 (f (cons u v) y 'a)) when rewriting y. See
  [patterned-congruence]. Thanks to Sol Swords for requesting this
  feature.


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

Fixed a small bug in xdoc/topics.lisp, in (defxdoc xdoc ...).

Made the following improvements pertaining to the ACL2-Doc Emacs
browser (some in acl2-devel, some in acl2-books):

  Files foo.acl2-doc will come up in ACL2-Doc mode, as requested by
  Warren (convenient for saving a file of bookmarks).

  Modified books/xdoc/display.lisp to print {IMAGE} or {ICON} for a
  missing image or icon (formerly these were just ignored when
  printing text).  Users should get the hint that these topics are
  best viewed on the web.

  A new ACL2-Doc command, H, displays the history in a special buffer.
  This can be convenient for revisiting topics.  Thanks to Nathan
  Wetzler for suggesting this improvement.

  A "type h for help" message now occurs at the bottom of the screen
  when starting up ACL2-Doc.

  A new ACL2-Doc command, D, forces a new download from the web of the
  acl2+books combined manual.

  The acl2-doc buffer is now in the directory of the file from which
  it was derived, as suggested by Warren.

  A new ACL2-Doc command, <Space>, is the same as Control-v (scroll
  up).

  Source information -- a book name or "ACL2 Sources" -- is now shown
  near the top of the page, when browsing the acl2+books combined
  manual with ACL2-Doc.

  If the combined manual exists in gzipped form only, say because it
  was manually downloaded from the web but not gunzipped, then at
  startup ACL2-Doc will offer to gunzip it.

  ACL2-Doc now displays which manual -- "acl2+books combined manual"
  or "ACL2 User's manual" -- at the bottom of the screen along with
  the topic name.

  A new command, <TAB>, tabs through the links on the displayed page.

  A failed attempts to download the combined manual may result in an
  improved error message.

  Fixed top page of the acl2+books combined manual to match what
  appears on the web, instead of being generic.


git-svn-id: http://acl2-books.googlecode.com/svn/trunk@2360 303c5b2c-9740-0410-b014-fd8f9db7be32
Minor tweak to :doc acl2-doc to reflect small change about to be checked into acl2-devel for emacs/acl2-doc.el.

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

Added links to ACL2-Doc, thanks to feedback from J.

Updated documentation for ACL2-Doc browser, based on change of
  control-x a a
to
  control-t g
and the addition of these (as explained in :doc acl2-doc):
  control-t G
  control-t control-t G
I've eliminated using the "control-x a" prefix because it's "owned" by
the "abbrev" mechanism, and I'm concerned that some day Emacs will
take over "control-x a a".  For now, control-x a a prints a helpful
error message, but I plan to remove this key binding after the next
release.



git-svn-id: http://acl2-books.googlecode.com/svn/trunk@2362 303c5b2c-9740-0410-b014-fd8f9db7be32
Minor Satlink changes
 - tweak riss3g-cert to use an additional option that is needed
 - extend config-check with a few more difficult problems
 - remove glucose testing stuff from config-check because it makes
   more sense to do it in satlink/solvers/
 - slightly tweak dimacs reader to permit out-of-range variable
   assignments, since they can arise when using riss3g and are harmless

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

Fixed :doc acl2-doc to reflect the following change, about to be
checked into acl2-devel:

Improved the ACL2-Doc "i" (index) command so that if you just hit
<RETURN>, then you go to the index buffer, which now is read-only and
is in ACL2-Doc mode (so that, for example, you can hit <RETURN> while
standing on a topic in order to be taken to that topic).


git-svn-id: http://acl2-books.googlecode.com/svn/trunk@2364 303c5b2c-9740-0410-b014-fd8f9db7be32
Various compatibility and documentation fixes

Arithmetic-5:
  - Rename (barely-used) "how-many" function to "how-many-factors,"
    to avoid name conflicts with other books, e.g., in sorting/

Bitops:
  - Rename |(integerp (expt x n))| rule to avoid name conflict with
    worse rule in arithmetic-5
  - Rename lognot-lognot to lognot-of-lognot, to avoid name conflicts
    with worse rules in arithmetic-5 and ihs/logops-lemmas

Documentation updates:
  - Documented def-universal-equiv
  - Extended def-universal-equiv with :parents, :short, :long
  - Documented centaur/misc/arith-equivs
  - Documented 4v-sexpr equivalences
  - Document recently added VL primitive modules
  - Enhanced documentation for set-max-mem
  - Fixed many, various broken links, etc
  - Remove obsolete vl ram-tools book from centaur/doc
  - Port vl/lint/stmtrewrite to define to fix its documentation

Satlink:
  - Minor tweaks to satlink literals (preferring "var" instead of "id")

XDOC:
  - xdoc-prepend now causes an error if you try to extend an undefined
    topic (like xdoc-extend does)
  - xdoc-extend and xdoc-prepend now tolerate extending topics with NIL
  - documented xdoc-extend and xdoc-prepend
  - avoid including stub book in unsound-eval-tests

Update issue 50

I documented xdoc-extend and prepend, so you can evaluate whether they
would suffice.

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

Added documentation for boolean-listp and read-acl2-oracle; thanks to
Jared Davis for the suggestions.

Fixed typo in cowles/LICENSE, as approved by John Cowles.


git-svn-id: http://acl2-books.googlecode.com/svn/trunk@2366 303c5b2c-9740-0410-b014-fd8f9db7be32
Makefile changes
 - Rename Makefile -> GNUmakefile
 - Add new Makefile with dummy targets for non-GNU makes (similar to
   how ACL2's Makefile works)

XDOC enhancements
 - Add support for basic <table> tags
 - Add support for <icon> tags, for small inline images, as opposed
   to <img> tags which are for big centered images (this mainly is
   to fix issues with the tour pages after changing how images are
   displayed by default)
 - Fixed bug with zip.sh that caused problems on Windows
 - Enhanced @(def ...) to say, e.g., "Theorem:", "Function:" or "Macro:",
   instead of just labeling everything as "Definition:"
 - Other minor xdoc code cleanup

Documentation updates
 - Patched up acl2-doc.lisp to use <icon> as appropriate
 - Updated note-6-4-books with information for some additional revisions
 - Other minor documentation updates

Miscellaneous:
 - Removed top-level README (which simply said to see Readme.html)

git-svn-id: http://acl2-books.googlecode.com/svn/trunk@2367 303c5b2c-9740-0410-b014-fd8f9db7be32
Patch mu-calculus to avoid package conflicts

git-svn-id: http://acl2-books.googlecode.com/svn/trunk@2368 303c5b2c-9740-0410-b014-fd8f9db7be32
Documentation updates
 - Update documentation regarding GNUmakefile instead of Makefile
 - Add some links to various community books
 - Fix up images (again) in the tours because I somehow botched
   the earlier commit
 - Slight reorganization of :doc books (in centaur/doc only)
 - Add set-max-mem comment to defung stress test book

git-svn-id: http://acl2-books.googlecode.com/svn/trunk@2369 303c5b2c-9740-0410-b014-fd8f9db7be32
VL updates (mostly for better documentation)
 - Modernize and document various functions, e.g., using define
 - Split fixing stuff out of checkers/duplicate-detect (--> mlib/fix)
 - Reduce dependencies in checkers/

Miscellaneous:
 - Mention ACL2-Doc from XDOC, better XDOC build instructions (with Matt)
 - Document str::hexify and str::binify
 - Other scattered doc fixes and updates

Other minor documentation updates

fix links

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

Removed superfluous comments in GNUmakefile about building an XDOC
manual.

Made some fixes to acl2-doc.lisp (in consultation with Jared, to avoid
some inadvertent recent changes).

Made minor updates to (defxdoc xdoc ...) in xdoc/topics.lisp.


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

[Using this commit message for both acl2-books and acl2-devel:]

For oracle-apply and oracle-fncall, we no longer prohibit the
function symbol from being SYNP, MV-LIST, or RETURN-LAST; the only
illegal function symbol is IF.  Also, quoting a comment in
(defxdoc note-6-4 ...):

; Synched up the guards of oracle-apply and ev-fncall-w, and removed
; untouchables check from ev-fncall-w (since that check is now in the guard).
; This could of course allow the user to do terrible things with ev-fncall-w
; when calling it from a :program mode function, but that's not really new.  At
; least untouchables won't be allowed for ev-fncall-w at the top level or when
; using safe-mode or guard-checking :all.


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

[Using this commit message for both acl2-books and acl2-devel:]

Updated :doc note-6-4 by adding the following paragraph, to reflect a
change made in the preceding commit:

  The [table] guard on [dive-into-macros-table] has been strengthened
  in order to avoid calling untouchable functions (see
  [remove-untouchable]).


git-svn-id: http://acl2-books.googlecode.com/svn/trunk@2373 303c5b2c-9740-0410-b014-fd8f9db7be32
Avoided problem handling stack overflow for CMUCL.

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

Fixed :doc acl2-doc to reflect the following changes, about to be
checked into acl2-devel:

Improved the ACL2-Doc "i" (index) command so that if you just hit
<RETURN>, then you go to the index buffer, which now is read-only and
is in ACL2-Doc mode (so that, for example, you can hit <RETURN> while
standing on a topic in order to be taken to that topic).

Modified :DOC broken-link for the ACL2-only manual so that it gives
specific information about the source books for missing documentation
links.


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

In GNUmakefile, allow overriding the SHELL variable by setting
ACL2_SHELL_OVERRIDE.  This capability would have been useful during a
conversation some weeks ago with Camm Maguire.

In GNUmakefile, modified the value of BOOKS_BKCHK_OUT to avoid
checking well-formedness of the world for problematic ccg/ccg.lisp
book.  Added comment to books/system/pseudo-good-worldp.lisp about
such exceptions.

[Using the rest of this commit message for both acl2-books and acl2-devel:]

Quoting :doc note-6-4:

  It had been possible to get a confusing raw Lisp error when
  submitting a [defstobj] event whose first argument is not a symbol,
  as in: (defstobj (fld :type integer :initially 0)). That user error
  is now reported gracefully by ACL2.

  When an [include-book] form is executed for a non-existent book, we
  no longer get a bogus warning about a missing compiled file. (Of
  course the compiled file is missing when the book itself is
  missing! So there's no need to report this fact.) Thanks to Caleb
  Eggensperger for bringing this issue to our attention.


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