[acl2/acl2] 9e5de1: Fixed package of "strengthen" function for (defun-...

[GitHub]

Branch: refs/heads/master
Home: https://github.com/acl2/acl2
Commit: 9e5de11e6b999dc8f601bd5bb264f8c9772cc549
https://github.com/acl2/acl2/commit/9e5de11e6b999dc8f601bd5bb264f8c9772cc549
Author: Matt Kaufmann <kauf...@cs.utexas.edu>
Date: 2016-07-29 (Fri, 29 Jul 2016)

Changed paths:
M books/system/doc/acl2-doc.lisp
M doc.lisp
M other-events.lisp

Log Message:
-----------
Fixed package of "strengthen" function for (defun-sk name ...) to be in the same package as name.

Quoting :doc note-7-3:

When [defun-sk] was supplied with keyword argument :strengthen t, the
name of the generated theorem was always in the "ACL2" package. Now
it is in the same package as the function symbol being defined.
Thanks to Alessandro Coglio for suggesting this change.

[GitHub]

Branch: refs/heads/testing