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

 Name                    Last modified      Size  Description
 Parent Directory                             -   
 CHANGES.html            28-Jan-2006 15:00  9.1K  
 COPYING                 12-Jun-2005 20:40   18K  
 Makefile                29-Jan-2006 19:45  1.4K  
 cert.acl2               12-Jun-2005 20:40   35   
 computed-hints.lisp     28-Jan-2006 14:23   15K  
 fast.lisp               28-Jan-2006 15:22   20K  
 instance.lisp           28-Jan-2006 14:27   23K  
 map.lisp                28-Jan-2006 14:23   14K  
 membership.lisp         28-Jan-2006 14:58   20K  
 outer.lisp              28-Jan-2006 14:42   14K  
 primitives.lisp         30-Jan-2006 21:51   14K  
 quantify.lisp           30-Jan-2006 21:53   28K  
 set-order.lisp          28-Jan-2006 14:24  4.3K  
 sets.defpkg             28-Jan-2006 14:24  1.6K  
 sets.lisp               16-Nov-2006 07:25   22K  
 sort.lisp               28-Jan-2006 14:54  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.