diff options
Diffstat (limited to 'books/workshops/2003/kaufmann/support/rtl/README')
| -rw-r--r-- | books/workshops/2003/kaufmann/support/rtl/README | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/books/workshops/2003/kaufmann/support/rtl/README b/books/workshops/2003/kaufmann/support/rtl/README new file mode 100644 index 0000000..e4f69df --- /dev/null +++ b/books/workshops/2003/kaufmann/support/rtl/README @@ -0,0 +1,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 + |