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

 Name                    Last modified      Size  Description
 Parent Directory                             -   
 Makefile                20-Sep-2004 20:24  699   
 aof.acl2                05-Jun-2000 00:12  1.6K  
 aof.lisp                19-Jan-2004 16:36   34K  
 certify.lsp             21-Apr-2000 12:44  1.5K  
 exercise1.acl2          09-Sep-2002 16:04   48   
 exercise1.lisp          01-Apr-2000 19:38  1.0K  
 exercise2.lisp          01-Apr-2000 19:39  2.1K  
 exercise3.lisp          15-Sep-2003 12:19  3.2K  
 exercise4a.lisp         01-Apr-2000 19:40  1.8K  
 exercise4b.lisp         01-Apr-2000 19:41  1.2K  
 exercise5.lisp          01-Apr-2000 19:33  7.0K  
 exercise6a.lisp         01-Apr-2000 19:35  1.4K  
 exercise6b.lisp         01-Apr-2000 19:35  1.7K  
 exercise7a.lisp         01-Apr-2000 19:36  1.3K  
 exercise7b.lisp         01-Apr-2000 19:43  2.0K  
 knuth-arch.lisp         15-Sep-2003 12:28   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