This README file explains how to read the examples in brr-input.lsp,
which support the paper "Advances in ACL2 Proof Debugging Tools" by
Matt Kaufmann and J Strother Moore.

File brr-input.lsp has input forms that are processed when certifying
the book, brr-book.lisp, which generates an output file identical to
file brr-log.txt.  So you may want to look at brr-log.txt to see what
is generated by brr-input.lsp.

Note:
This research was developed with funding from the Defense Advanced
Research Projects Agency (DARPA).  The views, opinions and/or findings
expressed are those of the authors and should not be interpreted as
representing the official views or policies of the Department of
Defense or the U.S. Government.  Released under Distribution Statement
``A'' (Approved for Public Release, Distribution Unlimited).