File: ground-zero.lisp

package info (click to toggle)
acl2 6.5-2
  • links: PTS
  • area: main
  • in suites: jessie, jessie-kfreebsd
  • size: 108,856 kB
  • ctags: 110,136
  • sloc: lisp: 1,492,565; xml: 7,958; perl: 3,682; sh: 2,103; cpp: 1,477; makefile: 1,470; ruby: 453; ansic: 358; csh: 125; java: 24; haskell: 17
file content (24 lines) | stat: -rw-r--r-- 706 bytes parent folder | download | duplicates (20) 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
 
(in-package "ACL2")
;includes changes to the default theory (mostly disabling built-in functions)

(in-theory (disable aref1))
(in-theory (disable aset1))
(in-theory (disable aref2))
(in-theory (disable aset2))
(in-theory (disable floor))
(in-theory (disable truncate))
(in-theory (disable mod))
(in-theory (disable rem))
(in-theory (disable expt))
(in-theory (disable ash))
(in-theory (disable binary-logand))
(in-theory (disable binary-logior))
(in-theory (disable binary-logxor))
(in-theory (disable binary-logeqv))
(in-theory (disable logorc1))
(in-theory (disable lognot))
(in-theory (disable evenp)) ;new
(in-theory (disable oddp)) ;new
(in-theory (disable nonnegative-integer-quotient)) ;new
;abs?