File: README

package info (click to toggle)
acl2 8.5dfsg-5
  • links: PTS
  • area: main
  • in suites: bookworm
  • size: 991,452 kB
  • sloc: lisp: 15,567,759; javascript: 22,820; cpp: 13,929; ansic: 12,092; perl: 7,150; java: 4,405; xml: 3,884; makefile: 3,507; sh: 3,187; ruby: 2,633; ml: 763; python: 746; yacc: 723; awk: 295; csh: 186; php: 171; lex: 154; tcl: 49; asm: 23; haskell: 17
file content (24 lines) | stat: -rw-r--r-- 731 bytes parent folder | download | duplicates (2) 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
 
A "makefile" is provided to certify the books included in this
directory. It is only necessary to run (GNU) make, possibly changing
the (make-)variable ACL2 to suit your needs. For example, you can use

% make

if the command acl2 starts ACL2 in your system, or

% make ACL2=your_acl2

in other cases.

There is another possibility for people using Emacs. It suffices to
type M-x compile RET to get the output in an Emacs compilation buffer.

A description of this work is available electronically at

http://www-cs.us.es/~imedina/polynomials.html

and in the following paper:

Medina-Bulo, I; Alonso-Jiménez, J. A. & Palomo-Lozano, F.
Automatic Verification of Polynomial Rings Fundamental Properties in ACL2
ACL2 Workshop 2000.