blob: bdff10ccd4739424df13a3dca4e963cc4b1bd325 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
|
_____________________________________________________________________
Fully Ordered Finite Sets for ACL2
Copyright (C) 2003, 2004 Kookamara LLC
Version 0.90 - 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 shoudl check to make
sure you have a recent copy.
Build Instructions
You must have ACL2 2.9 installed to build this library.
1. Edit the makefile.
- Change "include [...]/Makefile-generic" to point to the
file Makefile-generic in your acl2-sources/books
directory.
- Change "ACL2 = [...]/saved_acl2" to point to your ACL2
executable.
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.
|
