~ubuntu-branches/ubuntu/gutsy/acl2/gutsy

« back to all changes in this revision

Viewing changes to books/rtl/rel6/lib/README

• browse files at revision 7
• compare with another revision
• download diff
• download tarball
• view history from revision 7

Show diffs side-by-side

added

removed

books/rtl/rel6/lib/README

 

1

In order to include all books of the library, simply include the book

 

2

"lib/top".  (All of the "support" books may similarly be loaded via

 

3

the book "support/top".)  Alternatively, a subset of these books may

 

4

be loaded, according to the user's intentions.  In particular,

 

5

 

 

6

(1) "rtlarr" is needed only if arrays are involved in the application.

 

7

 

 

8

(2) "basic", "float", "reps", "round", "fadd", "brat" and "package-defs"

 

9

    are intended to be used specifically for floating-point applications.

 

10

 

 

11

(3) "util" has no effect on the proof process and may be omitted.

 

12

 

 

13

(4) "arith" contains a set of arithmetic rules that past users have found

 

14

     useful; it may be omitted or replaced by another ACL2 arithmetic package.

 

15

    (We recommend the package in the "arithmetic/" directory, since it enforces normal 

 

16

    forms which the rules in "lib/" may depend on.

• Older »

Loggerhead is a web-based interface for Breezy
Version: 2.0.1