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