
This directory contains some demos that you can run yourself.

To run the demos interactively, follow the instruction at the top of
the file "run.lisp", which may involve a little editing.

To run the demos in batch mode, do the editing specified at the top of
"run.lisp", and make sure that there is a shell command available
called "nqthm" that runs the Boyer-Moore theorem prover.  Then execute
the command

source script

in Unix.

If you have any questions, please feel free to contact me (Matt
Kaufmann) by email at kaufmann@cli.com.
