[acl2/acl2] 430e27: Fixed (declare (irrelevant ...)) bug. Improved :d...

[GitHub]

Branch: refs/heads/master
Home: https://github.com/acl2/acl2
Commit: 430e27459a6908ef35eede4b3038425273013e40
https://github.com/acl2/acl2/commit/430e27459a6908ef35eede4b3038425273013e40
Author: Matt Kaufmann <kauf...@cs.utexas.edu>
Date: 2016-09-27 (Tue, 27 Sep 2016)

Changed paths:
A books/kestrel/utilities/defthmr.lisp
M books/kestrel/utilities/top.lisp
M books/system/doc/acl2-doc.lisp
M defuns.lisp
M doc.lisp

Log Message:
-----------
Fixed (declare (irrelevant ...)) bug. Improved :doc meta-extract. Added defthmr and defthmdr. Added defthm as primary parent for :doc defthmd.

Fixed a bug in (declare (irrelevant ...)) that was introduced after
v7-2 when that declare form was first supported. Thanks to Eric Smith
for a helpful discussion.

Improved :doc meta-extract. Thanks to Sol Swords for his help (but
any remaining problems are solely due to me, of course).

Added new defthmr and defthmdr utilities to avoid errors from attempts
to create rewrite rules by default. Thanks to Eric Smith for helpful
discussions.

Added defthm as primary parent for :doc defthmd.

[GitHub]

Branch: refs/heads/testing