To recertify the exercise solutions, simply execute "make" in this directory
(assuming your system understands "make").  However, in order to recertify
the case study input, you will have to have built ACL2(r) (see :doc REAL) and
use make target all-plus, i.e., invoke "make all-plus".  If you want to
recertify the case study input, it may be preferable to do so in the
corresponding directory under the ACL2 distribution under books/nonstd/; see
../../../books/nonstd/README .

The case study input books are in subdirectory book/.  See book/README.  See
also book/outline/ for top-down outlines of various depths, as explained in the
case study article.

If you care to use the outline tool for your own work, please see the end of
book/README under the heading "USING THE PROOF OUTLINE TOOL."

The exercise solutions are in subdirectory solutions/.  See solutions/README.

Matt Kaufmann
Advanced Micro Devices, Inc.
June, 2000