[acl2/acl2] e073a4: Added new hints for using previously-proved termin...

[GitHub]

Branch: refs/heads/master
Home: https://github.com/acl2/acl2
Commit: e073a4418ccb04b5c7967c3e4971c901077e871f
https://github.com/acl2/acl2/commit/e073a4418ccb04b5c7967c3e4971c901077e871f
Author: Matt Kaufmann <kauf...@cs.utexas.edu>
Date: 2015-11-11 (Wed, 11 Nov 2015)

Changed paths:
M books/system/doc/acl2-doc.lisp
M defuns.lisp
M doc.lisp
M history-management.lisp
M prove.lisp
M tau.lisp

Log Message:
-----------
Added new hints for using previously-proved termination and guard theorems. Also fixed a bit of documentation.

Quoting :doc note-7-2:

It is now possible to give [hints] that specify the use of
termination or [guard] theorems for existing function symbols. See
[lemma-instance], [termination-theorem-example], and
[guard-theorem-example]. Thanks to Alessandro Coglio and Eric Smith
for requesting these features.

Also, fixed :doc functional-instantiation-example.

Also, the following was added to :doc note-7-2, but was actually
implemented in my preceding commit.

Warnings are no longer printed for :use hints applied to functional
instances of enabled rules. Thanks to Eric Smith for suggesting
this change.

[GitHub]

Branch: refs/heads/testing