Index of /users/moore/acl2/v3-4/distrib/acl2-sources/books/workshops/1999/knuth-91

 Name                    Last modified      Size  Description
 Parent Directory                             -   
 Makefile                17-Dec-2007 10:00  699   
 aof.acl2                17-Dec-2007 10:00  1.6K  
 aof.lisp                17-Dec-2007 10:00   34K  
 certify.lsp             17-Dec-2007 10:00  1.5K  
 exercise1.acl2          17-Dec-2007 10:00   48   
 exercise1.lisp          17-Dec-2007 10:00  1.0K  
 exercise2.lisp          17-Dec-2007 10:00  2.1K  
 exercise3.lisp          17-Dec-2007 10:00  3.2K  
 exercise4a.lisp         17-Dec-2007 10:00  1.8K  
 exercise4b.lisp         17-Dec-2007 10:00  1.2K  
 exercise5.lisp          17-Dec-2007 10:00  7.0K  
 exercise6a.lisp         17-Dec-2007 10:00  1.4K  
 exercise6b.lisp         17-Dec-2007 10:00  1.7K  
 exercise7a.lisp         17-Dec-2007 10:00  1.3K  
 exercise7b.lisp         17-Dec-2007 10:00  2.0K  
 knuth-arch.lisp         17-Dec-2007 10:00   43K  

The .lisp files in this directory can be certified on a Unix system by
executing make, assuming that this directory is directly under
books/case-studies in an ACL2 distribution,

Contents of this directory:

README           This file
certify.lsp      (ld "certify.lsp") to certify books aof and knuth-arch
aof.lisp         Axioms and rules for Archimedean Ordered Fields
knuth-arch.lisp  Theorems about Knuth's Generalized 91 Recursion

Answers to the exercises in the case study:
  exercise1.lisp
  exercise2.lisp
  exercise3.lisp    
  exercise4a.lisp
  exercise4b.lisp
  exercise5.lisp
  exercise6a.lisp    
  exercise6b.lisp    
  exercise7a.lisp    
  exercise7b.lisp