ACL2 Documentation
Generated by
cert2
ACL2 System
acl2-check
acl2-customization
acl2-fns
acl2-init
acl2-proclaims
acl2
akcl-acl2-trace
apply-constraints
apply-prim
apply
axioms
basis-a
basis-b
bdd
boot-strap-pass-2-a
boot-strap-pass-2-b
defpkgs
defthm
defuns
doc
float-a
float-b
history-management
hons
induct
init
ld
linear-a
linear-b
memoize
non-linear
other-events
other-processes
parallel
proof-builder-a
proof-builder-b
proof-builder-pkg
prove
rewrite
serialize
simplify
tau
translate
type-set-a
type-set-b
Books
portcullis
floor-mod-helper
floor-mod
cancel-terms-helper
cancel-terms-meta
collect-terms-meta
common-meta
expt-helper
expt
integerp-meta
integerp
mini-theories
non-linear
numerator-and-denominator
post
pre
top
basic-arithmetic-helper
basic-arithmetic
expt-helper
expt
inequalities
mini-theories
numerator-and-denominator-helper
numerator-and-denominator
prefer-times
top
arithmetic-theory
banner
basic-helper
basic
building-blocks
collect
common
default-hint
integerp-meta
integerp
mini-theories-helper
mini-theories
normalize
numerator-and-denominator
remove-weak-inequalities
simplify-helper
simplify
top
ext-compat
ext
top-ext
floor-mod
mod-expt-fast
basic-arithmetic-helper
basic-arithmetic
expt-helper
expt
inequalities
mini-theories
non-linear
num-and-denom-helper
numerator-and-denominator
prefer-times
top
top
arithmetic-theory
banner
basic
building-blocks-helper
building-blocks
collect
common
default-hint
distributivity
dynamic-e-d
elim-hint
expt-helper
expt
forcing-types
if-normalization
integerp-helper
integerp-meta
integerp
mini-theories
natp-posp
normalize
numerator-and-denominator
remove-weak-inequalities
simple-equalities-and-inequalities-helper
simple-equalities-and-inequalities
simplify-helper
simplify
top
types-helper
types
we-are-here
floor-mod-basic-helper
floor-mod-basic
floor-mod-helper
floor-mod
forcing-types
if-normalization
logand-helper
logand
mod-expt-fast
more-floor-mod
top
truncate-rem
basic-arithmetic-helper
basic-arithmetic
expt-helper
expt
inequalities
mini-theories
non-linear
num-and-denom-helper
numerator-and-denominator
prefer-times
top
top
abs
binomial
equalities
factorial
idiv
inequalities
mod-gcd
nat-listp
natp-posp
rational-listp
rationals
real-listp
realp
sumlist
top-with-meta
top
portcullis
driver-tests
driver
portcullis
scan
types
equal-by-logbitp
floor-mod
ihs-extensions
integer-length
logbitp-mismatch
portcullis
signed-byte-p
portcullis
baselists
basetypes
database
deftypes
docgen
fixequiv
fixtype
fty-alist
fty-list
fty-parseutils
fty-sugar
fty-sum-casemacro
fty-sum
fty-transsum
multicase
portcullis
top
visitor
portcullis
equal-sets
evaluator-metatheorems
memory-mgmt-logic
memory-mgmt
prev-stobj-binding
universal-equiv
witness-cp
fast
portcullis
pure
portcullis
equality
ev-find-rules
ev-theoremp
generalize
join-thms
magic-ev
meta-extract-user
remove-hyp
term-vars
unify-subst
use-by-hint
witness-cp
portcullis
acl2-agp
acl2-asg
acl2-crg
portcullis
alist-defthms
alist-defuns
alist-theory
array1
defalist
deflist
list-defthms
list-defuns
list-theory
no-duplicates
number-list-defthms
number-list-defuns
number-list-theory
portcullis
set-defthms
set-defuns
set-theory
structures
top
utilities
defsort
duplicated-members
generic
uniquep
@logops
basic-definitions
ihs-definitions
ihs-doc-topic
ihs-init
ihs-lemmas
ihs-theories
logops-definitions
logops-lemmas
math-lemmas
quotient-remainder-lemmas
alen1
aref1
array1p
aset1
bounded-integer-alistp
compress1
compress11
constants
default
dimensions
header
maximum-length
acons
alistp
assoc-equal
lookup-eq-def
lookup-eq
lookup-equal-def
remove-assoc-equal
strip-cars
symbol-alistp
complex
denominator
divide
floor
imagpart
integerp
less-than
minus
mod
nonnegative-integer-quotient
numerator
plus-and-minus
plus
realpart
times-and-divide
times
collect
disable
unsigned-byte-listp-def
portcullis
portcullis
baby-jubjub-subgroup-prime
bls12-381-prime
bn-254-group-prime
ed25519-base-prime
ed25519-group-prime
goldilocks-field-prime
jubjub-subgroup-prime
koala-bear
nist-p-256-base-prime
nist-p-256-group-prime
secp256k1-field-prime
secp256k1-group-prime
top
def-error-checker
ensure-function-is-guard-verified
ensure-function-is-logic-mode
ensure-list-has-no-duplicates
ensure-symbol-is-fresh-event-name
ensure-value-is-boolean
ensure-value-is-not-in-list
ensure-value-is-symbol-list
ensure-value-is-symbol
ensure-value-is-untranslated-term
applicability-conditions
cw-event
evmac-input-hints-p
fail-event
input-processing
make-event-terse
proof-preparation
restore-output
screen-printing
try-event
xdoc-constructors
channels
iprint-oracle-updates
read-object
typed-io-listp
fty-omap
fty-set
map
append
butlast
cdr
cons
intersection-equal
len
member-equal
no-duplicatesp-equal
nth
nthcdr
remove1-equal
revappend
reverse-list
take
true-list-fix
defprime
portcullis
portcullis
char
downcase
sublis-var-simple
all-digit-charsp
character-listp
make-character-list
acl2-count
assoc-keyword
chk-length-and-keys
coerce
defmacrodoc
defmacroq
defthmr
digit-to-char
enumerations
equal-of-booleans
er-soft-plus
top
explode-atom
explode-nonnegative-integer
intern-in-package-of-symbol
keyword-value-listp
keyword-value-lists
keyword-value-lists2
lookup-keyword
macro-args
make-termination-theorem
map-symbol-name
member-symbol-name
messages
msgp
myquotep
nat-to-string
ordinals
orelse
our-digit-char-p
pack
polarity
print-base-p
quote
read-acl2-oracle
state
strings
numbered-names
tables
trans-eval-error-triple
translate
update-acl2-oracle
acl2x-help
meta-plus-equal
meta-plus-lessp
meta-times-equal
meta
pseudo-termp-lemmas
term-defuns
term-lemmas
arithmetic-top-theory
bash-bsd
bash
beta-reduce
book-checks
callers-and-ancestors
character-encoding-test
check-acl2-exports
check-fn-inst
computed-hint-rewrite
computed-hint
csort
dead-events
defattach-bang
defattach-example
definline
defmac
defopener
defp
defpm
defproxy-test
defpun
defun-plus
dft-ex
dft
dijkstra-shortest-path
disassemble
dump-events
eliminate-irrelevance-tests
enumerate
equal-by-g-help
equal-by-g
eval
evalable-printing
expander-tests
expander
fast-coerce
fibonacci
file-io-doc
file-io
find-events-tests
find-lemmas
gentle
getprop
goodstein
grcd
hanoi
pkg1
pkg2
sub1
sub2
top
hons-help
hons-help2
hons-tests
how-to-prove-thms
install-not-normalized-tests
install-not-normalized
int-division
integer-type-set-test
invariants
meta-lemmas
mult
multi-v-uni
oprof
pigeonhole
priorities
problem13
process-book-readme
profiling
radix
random
records-bsd
records
records0
redef-pkg
rtl-untranslate
save-time
seq
seqw
simp
simplify-defuns
simplify-thm
sort-symbols
sticky-disable
symbol-btree
symbol-print-full-escapes
total-order-bsd
total-order
trace-star
transfinite
untranslate-patterns
wet
with-waterfall-parallelism
without-waterfall-parallelism
e0-ordinal
lexicographic-book
lexicographic-ordering-without-arithmetic
limits
ordinal-addition
ordinal-basic-thms
ordinal-definitions
ordinal-exponentiation
ordinal-isomorphism
ordinal-multiplication
ordinal-total-order
ordinals-without-arithmetic
top-with-meta
portcullis
read-acl2-oracle
apply
base
definductor
loop-lemmas
loop
relink-fancy-scion
top
euclid
fermat
portcullis
pratt
crt
euclid
euler
fermat
fta
gauss
mersenne
pratt
base
bordeaux
localize-macros
portcullis
basic
util
arith
arith2
basic
cg
common-factor-defuns
common-factor
complex-rationalp
denominator
even-odd
even-odd2-proofs
even-odd2
expo-proofs
expo
expt-proofs
expt
extra-rules
fl-expt
fl-hacks
fl-proofs
fl
floor-proofs
floor
fp2
ground-zero
induct
integerp
inverted-factor
mod-expt
mod-proofs
mod
negative-syntaxp
nniq
numerator
power2p
predicate
product-proofs
product
rationalp
top
unary-divide
x-2xx
convert-perm-to-how-many
how-many
merge-sort-term-order
perm
term-ordered-perms
abstract
alist-defuns
alist-equiv
alist-fix
alist-keys
alist-map-keys
alist-map-vals
alist-vals
alistp
alists-compatible
append-alist-keys
append-alist-vals
assoc
fal-all-boundp
fal-extract-vals
fal-extract
fal-find-any
fast-alist-clean
hons-assoc-equal
hons-put-assoc
hons-rassoc-equal
hons-remove-assoc
pairlis
put-assoc-equal
remove-assoc-equal
remove-assocs
strip-cars
strip-cdrs
top
worth-hashing
arith-equiv-defs
arith-equivs
bytep
code-char-char-code-with-force
controlled-configuration
defs
fix
good-pseudo-term-listp
good-pseudo-termp
good-valuep
if-star
ifix
inductions
intern-in-package-of-symbol
maybe-natp
maybe-string-fix
mbt-dollar
member-symbol-name
nfix
nibblep
nonkeyword-listp
organize-symbols-by-name
organize-symbols-by-pkg
pos-fix
realfix
rfix
symbol-name-lst
symbol-package-name-lst-tests
symbol-package-name-lst
symbol-package-name-non-cl-tests
symbol-package-name-non-cl
top
two-nats-measure
bignum-extract-opt-tests
bignum-extract-opt
bignum-extract
bits-between
bitsets-opt
bitsets
sbitsets-tests
sbitsets
top
base
combine
file-measure
nthcdr-bytes
open-channels
print-objects
read-file-bytes
read-file-characters-no-error
read-file-characters
read-file-lines-no-newlines
read-file-lines
read-file-objects
read-ints
read-string-light
read-string-tests
read-string
serialize-tests2
take-bytes
top
unsound-read
abstract
acl2-count
add-to-set
all-equalp
append
bits-equiv
butlast
duplicity
equiv
final-cdr
flatten
index-of
intersection
intersectp
last
len
list-defuns
list-fix
mfc-utils
nats-equiv
no-duplicatesp
nth
nthcdr
prefixp
rcons
remove-duplicates
remove
remove1-equal
repeat
resize-list
rev
revappend
reverse
same-lengthp
set-difference
sets
sublistp
subseq
suffixp
take
top
true-listp
union
update-nth
intern-in-package-of-symbol
two-nats-measure
core
portcullis
tests
top
with-fixing-theorems
assoc
compatiblep
core
delete
extensionality
from-alist
from-lists
portcullis
submap
tests
top
update
with-fixing-theorems
cardinality
computed-hints
delete
difference
element-list
instance
intersect
map-tests
map
membership
nonemptyp
outer
primitives
quantify-tests
quantify
sort
top
under-set-equiv
union
1d-arr
2d-arr
absstobjs
bitarr
clone
def-hash-theory
def-hash
natarr
nicestobj
stobj-table
stobjtab
1d-arr
2d-arr
clone
def-hash
top
updater-independence
abbrevs
arithmetic
ascii-chars
base64-tests
base64
bin-digit-char-listp
binary-tests
case-conversion
cat-base
cat
char-case
char-fix
char-kinds-tests
char-kinds
charset-fns
charset
coerce
dec-digit-char-listp
decimal-tests
decimal
defs-aux
defs-program
defs
digit-to-char
eqv
explode-atom
explode-implode-equalities
explode-nonnegative-integer
fast-cat
firstn-chars
hex-digit-char-listp
hex-tests
hex
hexify
html-encode
ieqv
iless
iprefixp
isort
istrpos
istrprefixp
isubstrp
lcletter-chars
lcletter-digit-chars
letter-chars
letter-digit-chars
letter-digit-dash-chars
letter-digit-uscore-chars
letter-digit-uscore-dash-chars
letter-digit-uscore-dollar-chars
letter-uscore-chars
letter-uscore-dollar-chars
make-character-list
nondigit-chars
oct-digit-char-listp
octal-tests
octal
pad
prefix-lines
pretty-defs-aux
pretty-defs
pretty-program
printable-chars
printtree-concat
printtree-fix
printtree-fty
printtree
stringify
stringless
strline-tests
strline
strnatless
strpos
strprefixp
strrange-equiv
strrpos
strsplit-tests
strsplit
strsubst-tests
strsubst
strtok-bang-tests
strtok-bang
strtok-tests
strtok
subseq
substrp
suffixp-tests
suffixp
symbols
top-doc
top
ucletter-chars
ucletter-digit-chars
url-encode-tests
url-encode
acceptable-rewrite-rule-p
add-suffix-lst
add-suffix-to-fn-lst
add-suffix-to-fn-or-const-lst
add-suffix-to-fn-or-const
all-fnnames
all-free-bound-vars-tests
all-free-bound-vars
all-lambdas-tests
all-lambdas
all-non-gv-exec-ffn-symbs-tests
all-non-gv-exec-ffn-symbs
all-non-gv-ffn-symbs-tests
all-non-gv-ffn-symbs
all-pkg-names-tests
all-pkg-names
all-program-ffn-symbs-tests
all-program-ffn-symbs
all-vars-in-untranslated-term
all-vars-open-tests
all-vars-open
all-vars
apply-fn-into-ifs-tests
apply-fn-into-ifs
apply-term-tests
apply-term
apply-terms-same-args-tests
apply-terms-same-args
apply-unary-to-terms-tests
apply-unary-to-terms
arglistp
arity-plus-tests
arity-plus
arity
check-and-call-tests
check-and-call
check-fn-call-tests
check-fn-call
check-if-call-tests
check-if-call
check-lambda-call-tests
check-lambda-call
check-list-call-tests
check-list-call
check-mbt-call-tests
check-mbt-call
check-mbt-dollar-call-tests
check-mbt-dollar-call
check-mv-let-call-tests
check-mv-let-call
check-nary-lambda-call-tests
check-nary-lambda-call
check-not-call-tests
check-not-call
check-or-call-tests
check-or-call
check-unary-lambda-call-tests
check-unary-lambda-call
check-user-lambda-tests
check-user-lambda
check-user-term-tests
check-user-term
classes-plus-tests
classes-plus
classes-tests
classes
close-lambdas-tests
close-lambdas
conjoin-equalities-tests
conjoin-equalities
conjoin
constant-namep-tests
constant-namep
constant-queries
constant-symbolp-tests
constant-symbolp
constant-value-tests
constant-value
defchoose-queries-tests
defchoose-queries
definedp-plus-tests
definedp-plus
definedp-tests
definedp
defun-sk-queries-tests
defun-sk-queries
dumb-negate-lit
dumb-occur-var-open-tests
dumb-occur-var-open
enhanced-utilities
event-landmark-names-tests
event-landmark-names
event-name-queries
fapply-term-tests
fapply-term
fapply-terms-same-args-tests
fapply-terms-same-args
fapply-unary-to-terms-tests
fapply-unary-to-terms
flatten-ands-in-lit
formals-plus-tests
formals-plus
fresh-logical-name-with-dollars-suffix
fresh-namep
fsubcor-var
fsublis-fn-tests
fsublis-fn
fsublis-var-more-theorems
fsublis-var-tests
fsublis-var
function-name-listp-tests
function-name-listp
function-namep-tests
function-namep
function-queries
function-symbol-listp-tests
function-symbol-listp
function-symbolp
fundef-disabledp-tests
fundef-disabledp
fundef-enabledp-tests
fundef-enabledp
genvar-dollar-tests
genvar-dollar
get-measure-plus-tests
get-measure-plus
get-measure-tests
get-measure
get-ruler-extenders-plus-tests
get-ruler-extenders-plus
get-ruler-extenders-tests
get-ruler-extenders
get-well-founded-relation-plus-tests
get-well-founded-relation-plus
get-well-founded-relation-tests
get-well-founded-relation
getprops
guard-theorem-no-simplify-dollar-tests
guard-theorem-no-simplify-dollar
guard-theorem-no-simplify-tests
guard-theorem-no-simplify
guard-verified-exec-fnsp-tests
guard-verified-exec-fnsp
guard-verified-fnsp-tests
guard-verified-fnsp
guard-verified-p-plus-tests
guard-verified-p-plus
guard-verified-p-tests
guard-verified-p
ibody-tests
ibody
if-tree-leaf-terms-tests
if-tree-leaf-terms
implicate
included-books-tests
included-books
induction-machine-plus-tests
induction-machine-plus
induction-machine-tests
induction-machine
install-not-normalized-dollar
install-not-normalized-event-tests
install-not-normalized-event
invariant-risk
irecursivep-plus-tests
irecursivep-plus
irecursivep-tests
irecursivep
irrelevant-formals-book
irrelevant-formals
known-packages-plus-tests
known-packages-plus
known-packages-tests
known-packages
lambda-closedp-tests
lambda-closedp
lambda-guard-verified-exec-fnsp-tests
lambda-guard-verified-exec-fnsp
lambda-guard-verified-fnsp-tests
lambda-guard-verified-fnsp
lambda-listp-tests
lambda-listp
lambda-logic-fnsp-tests
lambda-logic-fnsp
lambdap-tests
lambdap
logic-function-namep-tests
logic-function-namep
logical-name-listp-tests
logical-name-listp
macro-args-plus-tests
macro-args-plus
macro-keyword-args-plus-tests
macro-keyword-args-plus
macro-keyword-args-tests
macro-keyword-args
macro-name-listp-tests
macro-name-listp
macro-namep-tests
macro-namep
macro-queries
macro-required-args-plus-tests
macro-required-args-plus
macro-required-args-tests
macro-required-args
macro-symbol-listp-tests
macro-symbol-listp
macro-symbolp-tests
macro-symbolp
make-mv-let-call-tests
make-mv-let-call
make-mv-nth-calls-tests
make-mv-nth-calls
maybe-pseudo-event-formp-tests
maybe-pseudo-event-formp
measured-subset-plus-tests
measured-subset-plus
measured-subset-tests
measured-subset
mvify-tests
mvify
no-stobjs-p-plus-tests
no-stobjs-p-plus
no-stobjs-p-tests
no-stobjs-p
non-executablep-plus-tests
non-executablep-plus
non-executablep-tests
non-executablep
non-parallel-book
number-of-results-plus-tests
number-of-results-plus
number-of-results-tests
number-of-results
one-way-unify-dollar-tests
one-way-unify-dollar
partition-rest-and-keyword-args
plist-worldp-with-formals
primitivep-plus-tests
primitivep-plus
primitivep-tests
primitivep
pseudo-command-landmark-listp-tests
pseudo-command-landmark-listp
pseudo-event-form-fix
pseudo-event-form-listp-tests
pseudo-event-form-listp
pseudo-event-formp-tests
pseudo-event-formp
pseudo-event-landmark-listp-tests
pseudo-event-landmark-listp
pseudo-lambda-listp-tests
pseudo-lambda-listp
pseudo-lambdap-tests
pseudo-lambdap
pseudo-termfn-listp-tests
pseudo-termfn-listp
pseudo-termfnp-tests
pseudo-termfnp
pseudo-tests-and-call-listp-tests
pseudo-tests-and-call-listp
pseudo-tests-and-callp-tests
pseudo-tests-and-callp
pure-raw-p-tests
pure-raw-p
quote-term-list-tests
quote-term-list
quote-term-tests
quote-term
rawp-tests
rawp
recursive-calls-tests
recursive-calls
remove-dead-if-branches-tests
remove-dead-if-branches
remove-mbe-tests
remove-mbe
remove-progn-tests
remove-progn
remove-trivial-vars-tests
remove-trivial-vars
remove-unused-vars-tests
remove-unused-vars
rune-disabledp-tests
rune-disabledp
rune-enabledp-tests
rune-enabledp
stobjs-in-plus-tests
stobjs-in-plus
stobjs-out-plus-tests
stobjs-out-plus
table-alist-plus-tests
table-alist-plus
tail-recursive-p-tests
tail-recursive-p
term-function-recognizers
term-guard-obligation-tests
term-guard-obligation
term-possible-numbers-of-results-tests
term-possible-numbers-of-results
term-queries
term-transformations
termfn-listp-tests
termfn-listp
termfnp-tests
termfnp
termination-theorem-dollar-tests
termination-theorem-dollar
theorem-name-listp-tests
theorem-name-listp
theorem-namep-tests
theorem-namep
theorem-queries
theorem-symbol-listp-tests
theorem-symbol-listp
theorem-symbolp-tests
theorem-symbolp
thm-formula-plus-tests
thm-formula-plus
thm-formula-tests
thm-formula
top
ubody-plus-tests
ubody-plus
ubody-tests
ubody
uguard-plus-tests
uguard-plus
uguard-tests
uguard
unquote-term-tests
unquote-term
untranslate-dollar-tests
untranslate-dollar
unwrapped-nonexec-body-plus-tests
unwrapped-nonexec-body-plus
unwrapped-nonexec-body-tests
unwrapped-nonexec-body
w
assert-bang-stobj-tests
assert-bang-stobj
assert-bang-tests
assert-bang
assert-equal-tests
assert-equal
assert-qmark-tests
assert-qmark
assert
eval
must-be-redundant-tests
must-be-redundant
must-be-table-key
must-eval-to-t
must-eval-to
must-fail-local-tests
must-fail-local
must-fail-tests
must-fail-with-error
must-fail-with-hard-error
must-fail-with-soft-error
must-fail
must-not-be-table-key
must-not-prove
must-prove
must-succeed-star
must-succeed
top
top
cons-pos-alistp-tests
cons-pos-alistp
keyword-symbol-alistp-tests
keyword-symbol-alistp
keyword-to-keyword-value-list-alistp-tests
keyword-to-keyword-value-list-alistp
keyword-truelist-alistp
string-string-alistp-tests
string-string-alistp
string-stringlist-alistp
string-symbol-alistp
string-symbollist-alistp-tests
string-symbollist-alistp
symbol-alistp
symbol-nat-alistp-tests
symbol-nat-alistp
symbol-pos-alistp-tests
symbol-pos-alistp
symbol-pseudoeventform-alistp
symbol-pseudoterm-alistp-tests
symbol-pseudoterm-alistp
symbol-string-alistp-tests
symbol-string-alistp
symbol-symbol-alistp-tests
symbol-symbol-alistp
symbol-symbollist-alistp
symbol-truelist-alistp-tests
symbol-truelist-alistp
top
acl2-number-listp
atom-listp
boolean-listp
character-listp
cons-listp
eqlable-listp
integer-listp
nat-listp
portcullis
pseudo-term-listp
rational-listp
signed-byte-listp
string-listp
string-or-symbol-listp
symbol-listp
top
unsigned-byte-listp
add-io-pairs-tests-sub-1
add-io-pairs-tests-sub-2
add-io-pairs-tests-sub
add-io-pairs
bstar
cons
da-base
def-bound-theorems-tests
def-bound-theorems
defaggrify-defrec
defalist-base
defarbrec-doc
defarbrec-template
defarbrec
defconstrained-recognizer
defconsts
defenum-tests
defenum
deffixer
define-sk
defines
definj-doc
definj
defirrelevant-tests
defirrelevant
defiso-doc
defiso
deflist-aux
deflist-base
deflist
defmacro-plus-doc
defmacro-plus-tests
defmacro-plus
defmapping-doc
defmapping-proof-templates
defmapping-templates
defmapping-tests-concrete
defmapping-tests-template-1-1
defmapping-tests-template-1-2
defmapping-tests-template-2-1
defmapping-tests-template-2-2
defmapping-tests-utils
defmapping-tests-validation
defmapping
defmax-nat-doc
defmax-nat-template
defmax-nat-tests
defmax-nat
defmin-int-doc
defmin-int-template
defmin-int-tests
defmin-int
defmvtypes-tests
defmvtypes
defredundant-tests
defredundant
defret-mutual-generate
defretgen
defrule
defsum
defsurj-doc
defsurj
defthm-commutative
deftutorial-doc
deftutorial-tests
deftutorial
defund-sk-doc
defund-sk-tests
defund-sk
defval
error-value-tuples-tests
error-value-tuples
formals-tests
formals
generate-symbol
look-up-tests
look-up
maybe-defthm-tests
maybe-defthm
returnspecs-tests
returnspecs
support
termhints
bstar
defaggregate
defaggrify-defrec
defarbrec
define
defines
defmapappend
defprojection
defredundant
defval
top
utils
top
tuple
wizard
all-fnnames
apply-constraints
apply-prim-support
apply-prim
apply
bind-macro-args
case-match
convert-normalized-term-to-pairs
defstobj
acl2-doc
portcullis
extend-pathname
f-put-global
fmx-cw-support
fmx-cw
hl-addr-combine
kestrel
legal-variablep
merge-sort-symbol-lt
merge-sort-term-order
meta-extract
observation1-cw
origin
pseudo-command-formp
pseudo-command-landmarkp
pseudo-event-form-listp
pseudo-event-formp
pseudo-event-landmarkp
pseudo-good-worldp
pseudo-termp-lemmas
pseudo-tests-and-calls-listp
pseudo-tests-and-callsp
remove-guard-holders-weak
remove-guard-holders
remove-guard-holders1
subcor-var
sublis-var
subst-expr
subst-var
termp
top
verified-termination-and-guards
advise
bstar
btree
case-splitting-rules
clone-stobj
cws
dead-events
def-functional-instance
defevaluator-fast
define-keyed-function
defined-const
defmacfun
defsum
defthmg
defttag-muffled
deftuple
do-not
easy-simplify
elide-event-doc
elide-event
equality-with-hons-copy
er-soft-logic
eval-events-from-file-doc
eval-events-from-file-test
eval-events-from-file
fake-event
flag-tests
in-raw-mode
include-an-arithmetic-book
include-raw
k-induction
last-theory-change
lint
match-tree
memoize-prover-fns
mv-nth
names-after
nld
open-trace-file-bang
oracle-eval-real
oracle-eval
oracle-time
oracle-timelimit
pattern-match
plev-ccl
plev
doc
portcullis
top
prove-dollar-tests
prove-dollar
removable-runes
remove-hyps
rewrite-dollar-book
rewrite-dollar
rewrite-with-equality
rulesets
run-script
safe-case
save-obligs
saved-errors
show-diff-lines
some-events
stobj-frame
stobj-help
symlet
table-replay
templates
theory-tools
time-dollar-with-gc
top
trivial-ancestors-check
types-misc
untranslate-for-exec-tests
untranslate-for-exec
with-arith-help
with-arith1-help
with-arith5-help
with-quoted-forms
with-supporters-doc
with-supporters-test-sub
with-supporters-test-top
with-supporters
without-subsumption
autolink
base
book-thms
constructors
debug
defxdoc-plus
defxdoc-raw
display
fmt-to-str-orig
fmt-to-str
full-escape-symbol
init
names
parse-xml
prepare-topic
spellcheck
str
top
topics
unsound-eval
verbosep
word-wrap
xdoc-error