Index of /users/moore/acl2/v3-4/distrib/acl2-sources/books/finite-set-theory/osets

 Name                    Last modified      Size  Description
 Parent Directory                             -   
 CHANGES.html            17-Dec-2007 09:58  9.1K  
 COPYING                 17-Dec-2007 09:58   18K  
 Makefile                17-Dec-2007 09:58  1.4K  
 cert.acl2               17-Dec-2007 09:58   35   
 computed-hints.lisp     17-Dec-2007 09:58   15K  
 fast.lisp               17-Dec-2007 09:58   20K  
 instance.lisp           17-Dec-2007 09:58   23K  
 map.lisp                17-Dec-2007 09:58   14K  
 membership.lisp         17-Dec-2007 09:58   20K  
 outer.lisp              17-Dec-2007 09:58   14K  
 primitives.lisp         17-Dec-2007 09:58   14K  
 quantify.lisp           17-Dec-2007 09:58   28K  
 set-order.lisp          17-Dec-2007 09:58  4.3K  
 sets.defpkg             17-Dec-2007 09:58  1.6K  
 sets.lisp               17-Dec-2007 09:58   22K  
 sort.lisp               17-Dec-2007 09:58  7.9K  

_____________________________________________________________________

                 Fully Ordered Finite Sets for ACL2
               Copyright (C) 2003, 2004 by Jared Davis

                       Version 0.91 - README
_____________________________________________________________________


  About

    This is a finite set theory library for ACL2.

       ACL2 Home Page:
        - http://www.cs.utexas.edu/users/moore/acl2/

       Ordered Sets Home Page:
        - http://www.cs.utexas.edu/users/jared/osets/

    The home page includes documentation and information on the 
    latest and upcoming versions, and you should check to make
    sure you have a recent copy.
  
    This library is licensed under the GNU General Public License,
    see the file COPYING for more information.
  


  Build Instructions

    NOTE: You may already have a current copy of the library installed!
    Check your ACL2 distribution, under finite-set-theory/osets,
    to see what version of the library came with your copy of ACL2.
    Otherwise, here is how to build the library:

    1. Edit the makefile.

       - Change "include [...]/Makefile-generic" to point to the 
         file Makefile-generic in your acl2-sources/books 
         directory.

       - Change "ACL2 = acl2" to point to your ACL2 executable or
         script, typically "[...]/acl2-sources/saved_acl2"

    2. Run "make" to build the library.

       - Check to make sure that the following files were created:
         sets.cert, quantify.cert, set-order.cert, and map.cert.  
         If there was a problem, please send a report to 
         jared@cs.utexas.edu.

  All usage instructions are on the web page.