This is the README file for the ACL2 flying demo. The relevant files on this directory are:

If you wish to reproduce the demo on your local copy of ACL2, you should retrieve each of these files. Then certify the books noted above; certification instructions are included in each book. Then carry out the instructions in script.lisp.

Matt Kaufmann and J Strother Moore
June, 2000