Index of /users/moore/acl2/v3-0/distrib/acl2-sources/books/arithmetic

 Name                    Last modified      Size  Description
 Parent Directory                             -   
 Makefile                14-Mar-2005 12:49  1.4K  
 abs.lisp                20-Nov-2003 18:06  2.0K  
 binomial.lisp           15-Mar-2005 11:04   13K  
 certify.lsp             02-Jun-2004 19:17  2.5K  
 equalities.acl2         14-Mar-2005 12:35  469   
 equalities.lisp         01-Feb-2004 10:59   24K  
 factorial.lisp          20-Nov-2003 18:06  1.0K  
 idiv.lisp               20-Nov-2003 18:06  4.6K  
 inequalities.lisp       20-Nov-2003 18:06   19K  
 mod-gcd.lisp            20-Nov-2003 18:06   19K  
 natp-posp.lisp          14-Feb-2005 10:51  3.8K  
 rational-listp.lisp     20-Nov-2003 18:06  1.3K  
 rationals.lisp          20-Nov-2003 18:06  8.9K  
 sumlist.lisp            15-Mar-2005 11:16  952   
 top-with-meta.lisp      20-Nov-2003 18:06  1.0K  
 top.lisp                20-Nov-2003 18:16  1.4K  

Contents of this directory:

README			This file
abs.lisp		Theorems about absolute value
binomial.lisp		A proof of the binomial theorem
certify.lsp		(ld "certify.lsp") to certify books in this directory
equalities.lisp		Arithmetic equality rules
factorial.lisp		Theorems about the factorial function
idiv.lisp		Theorems about integer division and related functions
inequalities.lisp	Arithmetic inequality rules
rational-listp.lisp	Very short book about lists of rationals
rationals-with-axioms-proved.lisp	Supersedes rationals-with-axioms.lis
sumlist.lisp		Theorems about sum of a list of numbers
top.lisp		Putting it all together
top-with-meta.lisp      Extension of top.lisp by the books in ../meta

Many people contributed to these books, especially

  Bishop Brock
  John Cowles
  Matt Kaufmann  
  Art Flatau
  Ruben Gamboa