Updated license/copyright as approved by Robert Krug.
Miscellanous :doc: improved proof-checker command topics (e.g. by adding proper links), documented misc/find-lemmas, documented unquote.

I also added a pointer to Emacs command control-t d in :doc
acl2-pc::dv, and to control-t control-d in :doc acl2-pc::dive.
Fixed a bug in the handling of hidden packages by encapsulate forms.

Quoting :doc note-7-0:

  There was a bug in how so-called ``hidden packages'' were handled by
  [encapsulate] forms (see [hidden-death-package]), which was
  preventing package axioms from being visible in certain contexts.
  (Technical remark: packages that were hidden after the second pass
  but not the first were treated as not-hidden, even though their
  package axioms were not introduced.) That, in turn, could cause an
  [include-book] form to fail when the book contains a
  [deftheory-static] form. Here is an example failure. First, in a
  fresh ACL2 session evaluate the form (defpkg "FOO" nil) and then
  evaluate the form (certify-book "foo" 1), where file foo.lisp is as
  follows.

    (in-package "ACL2")
    (defun foo::foo (x) x)
    (deftheory-static foo-theory
      (current-theory :here))

  Now evaluate the following sequence of forms. In previous versions of
  ACL2, the final ([include-book]) form failed.

    (encapsulate () (local (include-book "foo")) (defun h (x) x))
    (encapsulate () (local (include-book "foo")) (defun h2 (x) x))
    (include-book "foo") ; failed before the fix
Print failure message when error output is not inhibited, even if summary output is.

Quoting :doc note-7-0:

  In the case that summary output is inhibited but error output is not
  (see [set-inhibited-summary-types]), failed [events] did not print
  an error message. Now they do.
Added to a .gitignore for Mac.