===========
	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;

  2. 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