summaryrefslogtreecommitdiff
path: root/books/workshops/2003/kaufmann/support/rtl/README
blob: e4f69dfd34a71a72c40dfd1991b231c16e2f5307 (plain)
1
2
3
4
5
6
7
8
Type "make" to generate and certify files in the current directory that should
agree with the files in the results/ subdirectory, essentially:

model.lisp      simplified version of input file model-raw.lisp
model-eq.lisp   proofs of equivalence of model-raw and model functions
bvecp.lisp      proofs of bvecp lemmas about model functions, originally proved
                for model-raw functions