Index of /users/jared/osets/Distributions/osets-0.91
Name Last modified Size Description
Parent Directory -
CHANGES.html 25-May-2007 12:30 9.1K
COPYING 25-May-2007 12:30 18K
Makefile 25-May-2007 12:30 1.1K
cert.acl2 25-May-2007 12:30 35
computed-hints.cert 25-May-2007 12:30 959
computed-hints.date 25-May-2007 12:30 29
computed-hints.lisp 25-May-2007 12:30 15K
computed-hints.out 25-May-2007 12:30 6.0K
fast.cert 25-May-2007 12:30 1.3K
fast.date 25-May-2007 12:30 29
fast.lisp 25-May-2007 12:30 20K
fast.out 25-May-2007 12:30 34K
instance.cert 25-May-2007 12:30 807
instance.date 25-May-2007 12:30 29
instance.lisp 25-May-2007 12:30 23K
instance.out 25-May-2007 12:30 8.2K
map.cert 25-May-2007 12:30 2.0K
map.date 25-May-2007 12:30 29
map.lisp 25-May-2007 12:30 14K
map.out 25-May-2007 12:30 59K
membership.cert 25-May-2007 12:30 1.2K
membership.date 25-May-2007 12:30 29
membership.lisp 25-May-2007 12:30 20K
membership.out 25-May-2007 12:30 36K
outer.cert 25-May-2007 12:30 1.4K
outer.date 25-May-2007 12:30 29
outer.lisp 25-May-2007 12:30 14K
outer.out 25-May-2007 12:30 146K
primitives.cert 25-May-2007 12:30 812
primitives.date 25-May-2007 12:30 29
primitives.lisp 25-May-2007 12:30 14K
primitives.out 25-May-2007 12:30 27K
quantify.cert 25-May-2007 12:30 1.9K
quantify.date 25-May-2007 12:30 29
quantify.lisp 25-May-2007 12:30 28K
quantify.out 25-May-2007 12:30 59K
set-order.cert 25-May-2007 12:30 2.3K
set-order.date 25-May-2007 12:30 29
set-order.lisp 25-May-2007 12:30 4.3K
set-order.out 25-May-2007 12:30 9.1K
sets.cert 25-May-2007 12:30 1.7K
sets.date 25-May-2007 12:30 29
sets.defpkg 25-May-2007 12:30 1.6K
sets.lisp 25-May-2007 12:30 22K
sets.out 25-May-2007 12:30 32K
sort.cert 25-May-2007 12:30 1.6K
sort.date 25-May-2007 12:30 29
sort.lisp 25-May-2007 12:30 7.9K
sort.out 25-May-2007 12:30 28K
_____________________________________________________________________
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.