===========
	Ivy sources
	===========

Files:

  Makefile          :
  *.lisp            : the books
  Certify.lisp      : ACL2 commands to certify all the books
  Include-graph.ps  : a graph showing the include-structure of the books

Subdirectories:

  util              : Common Lisp code for the external-prover interface,
                    : and scripts for running Ivy
  test              : a few simple tests of Ivy
  examples          : more tests of Ivy
  exercises         : exercises and solutions

To certify all of the books,

  1. make sure the pathname in arithmetic.lisp is correct (unless this
     directory comes from the ACL2 distribution and has not been moved relative
     to that distribution)

  2. Type make on a Unix system.  Otherwise:
     acl2 < Certify.lisp > Certify.out
     This takes almost 90 minutes on a PII-400 Linux box and
     generates about 23 megabytes of output.

To run Ivy, see

  test/README
  examples/README

The entire Ivy distribution, which includes mace-1.3.4 and otter-3.0.6 (but is
not included in the ACL2 distribution), may be found at:

  http://www.mcs.anl.gov/~mccune/acl2/ivy/ivy-v2.tar.gz