[acl2/acl2] 7bff92: Improved :doc quicklisp. Remove-hyps handles let,...

[GitHub]

Branch: refs/heads/master
Home: https://github.com/acl2/acl2
Commit: 7bff925dcf6d07a830820615dba973e7d5e70aa4
https://github.com/acl2/acl2/commit/7bff925dcf6d07a830820615dba973e7d5e70aa4
Author: Matt Kaufmann <matthew.j...@gmail.com>
Date: 2016-11-21 (Mon, 21 Nov 2016)

Changed paths:
M books/centaur/quicklisp/top.lisp
M books/misc/bash.lisp
M books/system/doc/acl2-doc.lisp
M books/tools/remove-hyps.lisp
M doc.lisp
M hons-raw.lisp
M proof-builder-b.lisp

Log Message:
-----------
Improved :doc quicklisp. Remove-hyps handles let, let*, defthm, and thm. Proof-builder bash and reduce tolerate (and ignore) :do-not-induct t. Slow-alist-warning is improved.

Improved :doc quicklisp (to close github Issue #669).

Improved remove-hyps to handle let and let* expressions, as well as
defthmd and thm.

Quoting :doc note-7-3:

The [proof-builder]'s bash and reduce commands no longer fail when
the :hints for "Goal" include :do-not-induct t. Thus, it is no
longer necessary to edit out such :do-not-induct [hints] when
editing a proof-builder command by copying hints from an event
being developed.

The slow-alist warning and its documentation (see
[slow-alist-warning]) have been improved. Now, we mention in the
warning that one can break on the warning; thanks to Keshav Kini
for a conversation leading to that change. Also, the warning now
mentions a user-friendly version of the caller's name (for example,
HONS-GET rather than HL-HSPACE-HONS-GET).

[GitHub]

Branch: refs/heads/testing