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

 Name                    Last modified      Size  Description
 Parent Directory                             -   
 Makefile                20-Jul-2009 18:13  669   
 aof.acl2                13-Oct-2008 14:04  1.6K  
 aof.lisp                13-Oct-2008 14:04   34K  
 certify.lsp             13-Oct-2008 14:04  1.5K  
 exercise1.acl2          13-Oct-2008 14:04   48   
 exercise1.lisp          13-Oct-2008 14:04  1.0K  
 exercise2.lisp          13-Oct-2008 14:04  2.1K  
 exercise3.lisp          13-Oct-2008 14:04  3.2K  
 exercise4a.lisp         13-Oct-2008 14:04  1.8K  
 exercise4b.lisp         13-Oct-2008 14:04  1.2K  
 exercise5.lisp          13-Oct-2008 14:04  7.0K  
 exercise6a.lisp         13-Oct-2008 14:04  1.4K  
 exercise6b.lisp         13-Oct-2008 14:04  1.7K  
 exercise7a.lisp         13-Oct-2008 14:04  1.3K  
 exercise7b.lisp         13-Oct-2008 14:04  2.0K  
 knuth-arch.lisp         13-Oct-2008 14:04   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