Made further improvements to invariant-risk handling.  For one thing,
mv-let-for-with-local-stobj had a soundness bug (introduced after
Version 6.4):

  (in-package "ACL2")

  (defstobj st fld)

  (defun foo ()
    (declare (xargs :verify-guards nil))
    (with-local-stobj
     st
     (mv-let (result st)
	     (mv (mbe :logic 'logic :exec 'exec) st)
	     result)))

  (defthm wrong
    (equal (foo) 'logic)
    :hints (("Goal" :in-theory (disable (foo))))
    :rule-classes nil)

  (defthm contradiction
    nil
    :hints (("Goal" :use wrong))
    :rule-classes nil)

For another bug, see the comment at the end of this sequence of
events.

  (defun f-log () (mbe :logic 'logic :exec 'exec))
  (defstobj st (fld :type integer :initially 0))
  (defun f-prog (st)
    (declare (xargs :stobjs st :mode :program))
    (let ((st (update-fld 3 st)))
      (mv (f-log) st)))
  (f-prog st)
  (defun f-prog2 (st)
    (declare (xargs :stobjs st :mode :program))
    (let ((st (update-fld 3 st)))
      (mv (ec-call (f-log)) st)))
  ; The following should return
  ; (LOGIC <st>)
  ; and now it does, but previously it returned
  ; (EXEC <st>).
  (f-prog2 st)

Also, improved comments and :doc note-6-5 item about invariant-risk.

As far as I know, invariant-risk handling is perfect (!) now.  But I
may look into speeding up code.  Consider event MAX6-PROOF from
books/workshops/2009/sumners/support/examples.lisp.  The time reported
on my laptop has been (and I think this is virtually the same
regardless of whether we use ACL2(h) before or after this check-in).

; 29.21 seconds realtime, 26.03 seconds runtime
; (4,772,821,600 bytes allocated).

But if first I execute (setq *ignore-invariant-risk* t) in raw Lisp,
to defeat handling of invariant-risk (by restricting some execution to
*1* functions), then I get:

; 0.66 seconds realtime, 0.16 seconds runtime
; (24,119,776 bytes allocated).


git-svn-id: http://acl2-devel.googlecode.com/svn/trunk@1355 5d84a466-a78b-0930-a311-59b22171a541
Updating doc.lisp for invariant-risk change to :doc note-6-5 in books/system/doc/acl2-doc.lisp

git-svn-id: http://acl2-devel.googlecode.com/svn/trunk@1356 5d84a466-a78b-0930-a311-59b22171a541
Added guard to all-but-last and put it in guard-verified :logic mode, as requested by Warren Hunt.

git-svn-id: http://acl2-devel.googlecode.com/svn/trunk@1357 5d84a466-a78b-0930-a311-59b22171a541