Modified the addition to :doc note-6-5 from the preceding check-in.
The change this time is that when a :program mode function calls the
*1* function for a :logic mode function because of the risk of an
ill-guarded stobj update, nevertheless an mbe call under that :logic
mode function will lead to evaluation of the :exec code, not the
:logic code.  As noted below, there is a (long) comment about this in
(defxdoc note-6-5 ...).

  Some evaluations of forms (mbe :logic L :exec E) are more efficient
  or avoid guard violations, by evaluation of the :exec form (E)
  instead of the :logic form (L). If the [mbe] call is in a
  :[program] mode function definition, the :exec code will be
  evaluated, where unlike before, this is true even when
  guard-checking is :all or :none (see [set-guard-checking]). If the
  mbe call is in a :[logic] mode function definition, the change is
  that the :exec code will be evaluated when there is a superior call
  of a :program mode function, except when guard-checking is :all or
  :none; this had failed to be the case in cases where there was an
  ``invariant-risk'' of ill-guarded stobj updates. However, there is
  no change in the case of safe-mode, which is used during evaluation
  of [defconst], [value-triple], and [defpkg] forms, and during
  macroexpansion: the :logic and :exec forms are still both evaluated
  and checked for equality. Thanks to Jared Davis for reporting this
  issue and for helpful chats about it. For more information, see the
  comment about ``mbe and invariant-risk'' in the form (defxdoc
  note-6-5 ...) in [community-books] file
  books/system/doc/acl2-doc.lisp.

Made additional minor change to raw-ev-fncall other than one in
support of the change above, that might help a bit with function
proclaiming.

Made additional minor tweaks to oneify-cltl-code in the process of
modifying it to support the change documented above.

Fixed a bug in with-base-10, which had used eq instead of eql to
compare numbers.

[Note: it remains to update doc.lisp to reflect
books/system/doc/acl2-doc.lisp changes.  I plan to fix that today.]
Changed :doc mbe and :doc note-6-5, to reflect check-in to
acl2-devel svn revision 1308.
Incorporated into :doc linear-arithmetic an improvement suggested by
Ben Selfridge (and did a bit of reformatting while I was at it).
Updated doc.lisp to match updates to books/system/doc/acl2-doc.lisp
(made in acl2-books revisions revision 2788 and 2789).

Removed a bit of dead code and adjusted a comment accordingly.
Addressing slowdown in Allegro that _might_ be due to recent commits.
Quoting a comment in rewrite-free-theory, file ihs/ihs-init.lisp:

; Change by Matt K. mod, 6/9/2014: The use of set-difference-equal here and/or
; in definition-free-theory caused a stack overflow in Allegro CL.  Even in
; CCL, we found that it took over 10 seconds on a reasonably modern machine to
; evaluate the form
; (rewrite-free-theory (definition-free-theory (universal-theory 'ihs-theories)))
; after
; (include-book "centaur/vl/top" :dir :system)
; and
; (include-book "ihs/ihs-theories" :dir :system).
; After the change to this function and definition-free-theory, the time was
; reduced to 0.05 seconds (realtime and runtime) -- reduction by more than two
; orders of magnitude!  The above evaluation produced the same result, up to
; ordering, after the changes.
Improved error message when calling ec-call on a macro call, in the
case that the macro is a macro-alias.
VL updates to support typedefs

  - Added basic representations of data types, typedefs
  - Added parsing support and basic parsing unit tests

However, there's not yet any kind of semantic checking of typedefs, and no
transforms know about them yet.
VL: add support for SystemVerilog 'endmodule : foo' module endings.

Fix minor typo in seq documentation.
Minor VL fixes and extensions
  - fix up vl-preprocess so that filemaps properly include `included files
  - extend parser to support top-level parameters and localparameters
  - remove inappropriate fast-alist-free from vl-filter-modinsts-by-modname+
  - remove deprecated override options from various vl commamnds
  - add include-dirs option to various vl commands
VL: get rid of deprecated overrides stuff
Ignoring some files. Thanks for the clear instructions in README-svn Matt.
Ignoring some files. Thanks for the clear instructions in README-svn Matt.
Ignoring some files. Thanks for the clear instructions in README-svn Matt.
Ignoring some files. Thanks for the clear instructions in README-svn Matt.
Ignoring some files. Thanks for the clear instructions in README-svn Matt.
Read hons-raw.lisp carefully, asked Jared Davis some questions (which
he answered), and made a few small edits.  I am now happy to take
responsibility for that file (though so far I'm only speaking for
myself, not J), as has been the plan.  It remains to deal similarly
with memoize-raw.lisp, and to get agreement with J, before we consider
ACL2(h) not to be "experimental".  Thanks to Jared Davis for his help!

Note that a few small additional changes may come soon.  This commit
is intended to reflect only very small changes based on a careful read
of hons-raw.lisp.
Slightly optimized add-linear-lemma (extra case explicitly for when
linearization produced nil).

Made a couple of trivial comment fixes.
Reverting hons-raw.lisp to revision 1310 until I figure out why certification is failing (even after building quicklisp) for books/system/doc/acl2-manual.lisp.
Restored the new hons-raw.lisp checked in at revision 1311, but with a bug fix this time.