Improving the 'why' macro with a new version of it, why-explain, that monitors and prints an appromixation of the related checkpoint when the hypothesis fails to be relieved.

git-svn-id: http://acl2-books.googlecode.com/svn/trunk@2509 303c5b2c-9740-0410-b014-fd8f9db7be32
Forking jared-customization.lsp so that we can have something that's more officially part of 'the standard approach'.

Fixes issue 150

git-svn-id: http://acl2-books.googlecode.com/svn/trunk@2510 303c5b2c-9740-0410-b014-fd8f9db7be32
Tweaks to define/defines and new book to automate certain common proofs:
 - Define/defines: use with-output to remove a lot of the printing
 - Defines: Prove return types all together by (flag) induction, and add
            option to turn this off (prove all separately)
 - Add fixtype book (and fixtype-tests) to reduce boilerplate for proofs
            that e.g. (foo (jfix x)) = (foo x) and therefore
            foo has a jfix-equiv congruence

git-svn-id: http://acl2-books.googlecode.com/svn/trunk@2511 303c5b2c-9740-0410-b014-fd8f9db7be32
XDOC: implemented subtopic ordering (fixes issue 139)
STD: minor package tweaks
Fix memoize-flush issue in nrev

git-svn-id: http://acl2-books.googlecode.com/svn/trunk@2512 303c5b2c-9740-0410-b014-fd8f9db7be32