LICENSE
README
TAGS
acl2-check.lisp
acl2-fns.lisp
acl2-init.lisp
acl2.lisp
akcl-acl2-trace.lisp
all-files.txt
axioms.lisp
basis.lisp
bdd.lisp
books
defpkgs.lisp
defthm.lisp
defuns.lisp
doc
emacs
enable-eval.lisp
# ftp-images-README -- not for distribution
# ftp-script.v1-8 -- not for distribution
gcl-patch.lisp
history-management.lisp
induct.lisp
init.lsp
interface
interface-raw.lisp
ld.lisp
# logeqv-compile.wfasl is a Lispworks patch; don't know if we may distribute
makefile
mcl-acl2-startup.lisp
other-events.lisp
other-processes.lisp
p.lisp
proof-checker-a.lisp
proof-checker-b.lisp
proof-checker-pkg.lisp
prove.lisp
# release.txt -- Not for distribution.  Use this when making an ACL2 release.
reports
rewrite.lisp
saved
simplify.lisp
sum-list-example.lisp
translate.lisp
tutorial.lisp
type-set-a.lisp
type-set-b.lisp

books:
README
arithmetic
bdd
certify-numbers.lisp
cowles
makefile
meta
nqthm
public

books/arithmetic:
README
certify.lisp
equalities.lisp
inequalities.lisp
rational-listp.lisp
rationals-with-axioms.lisp
top-with-meta.lisp
top.lisp

books/bdd:
README
alu-proofs.lisp
alu.lisp
bdd-primitives.lisp
be
benchmarks.lisp
bit-vector-reader.lisp
bool-ops.lisp
cbf.lisp
# certify -- Not for distribution, but handy for testing BDDs
certify.lisp
hamming.lisp
# init.lsp -- see the README above
pg-theory.lisp

books/bdd/be:
cath
ex

books/bdd/be/cath:
add1.be
add2.be
add3.be
add4.be
addsub.be

books/bdd/be/ex:
mul03.be
mul04.be
mul05.be
mul06.be
mul07.be
mul08.be
rip02.be
rip04.be
rip06.be
rip08.be
transp.be
ztwaalf1.be
ztwaalf2.be

books/cowles:
acl2-agp.lisp
acl2-asg.lisp
acl2-crg.lisp
certify.lisp

books/meta:
README
certify.lisp
meta-generic-plus.lisp
meta-plus-equal.lisp
meta-plus-lessp.lisp
meta-plus.lisp
meta-times-equal.lisp
meta.lisp
pseudo-termp-lemmas.lisp
term-defuns.lisp
term-lemmas.lisp

books/nqthm:
README
certify.lisp
embedding.lisp
functions-and-axioms.lisp
more-functions.lisp
nqthm.lisp
proveall.lisp
rules1.lisp
rules2.lisp

books/public:
README
acl2-customization.lisp
alist-defthms.lisp
alist-defuns.lisp
alist-theory.lisp
defalist.acl2
defalist.lisp
define-structures-package.lisp
define-u-package.lisp
deflist.acl2
deflist.lisp
list-defthms.lisp
list-defuns.lisp
list-theory.lisp
makefile
sets.lisp
structures.acl2
structures.lisp
typed-lists.lisp
utilities.acl2
utilities.lisp

doc:
EMACS
HTML
LEMACS
README
TEX
create-acl2-html
create-acl2-texinfo
make-texinfo.el
texinfo.tex
write-acl2-html.lisp
write-acl2-texinfo.lisp

doc/EMACS:
acl2-doc-emacs.info
acl2-doc-emacs.info-*
saved

doc/EMACS/saved:

doc/HTML:
acl2-doc-*.html
acl2-doc.html
saved

doc/HTML/saved:

doc/LEMACS:
acl2-doc-lemacs.info
acl2-doc-lemacs.info-*
saved

doc/LEMACS/saved:

doc/TEX:
acl2-book.dvi.Z
acl2-book.ps.Z
saved

doc/TEX/saved:

emacs:
README
acldoc.el
compare-files.lisp
doc-notes.txt
emacs-stuff.el
fill-tildes.el

interface:
emacs
infix

interface/emacs:
README.doc
README.mss
README.ps
acl2-interface-functions.el
acl2-interface.el
acl2-mode.el
inf-acl2.el
interface-macros.el
key-interface.el
load-inferior-acl2.el
load-shell-acl2.el
mfm-acl2.el
mfm.el
top-start-inferior-acl2.el
top-start-shell-acl2.el

interface/infix:
CLI.sty
README
acl2-formatting.lisp
doinfix
infix.lisp
latex-init.lisp
latex-theory.lisp
makefile
scribe-init.lisp
scribe-theory.lisp
sloop.lisp

reports:
acl2-design.ps
acl2-design.tex
note-215-acl2-advantages.bib
note-215-acl2-advantages.mss
note-215-acl2-advantages.ps
story.txt

saved: