; Contents of this directory:
; 
; Readme.lsp              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

; ACL2-readable data:

((:FILES ; non-empty list of filenames, generated from Unix command "ls -1R"
"
.:
Makefile
Readme.lsp
abs.lisp
binomial.lisp
certify.lsp
equalities.acl2
equalities.lisp
factorial.lisp
idiv.lisp
inequalities.lisp
mod-gcd.lisp
natp-posp.lisp
rational-listp.lisp
rationals.lisp
sumlist.lisp
top-with-meta.lisp
top.lisp
")
 (:TITLE    "Arithmetic")
 (:AUTHOR/S ; non-empty list of author strings
  "Bishop Brock"
  "John Cowles"
  "Matt Kaufmann"
  "Art Flatau"
  "Ruben Gamboa"
  )
 (:KEYWORDS ; non-empty list of keywords, case-insensitive
   "arithmetic" "abs" "binomial" "equalities" "factorial" "idiv" "division"
   "integer division" "inequalities" "rationals" "sumlist"
   )
 (:ABSTRACT "
This directory contains books to help in proving theorems about arithmetic.
See also arithmetic-3/ for an alternate arithmetic library."))