` `

(often cited in more accessible documentation)
Major Section: ACL2 Documentation

### ABORT! -- to return to the top-level of ACL2's command loop

### ACCUMULATED-PERSISTENCE -- to get statistics on which runes are being tried

### ACKNOWLEDGMENTS -- some contributors to the well-being of ACL2

### ACL2-COUNT -- a commonly used measure for justifying recursion

### ACL2-CUSTOMIZATION -- customizing ACL2 for a particular user

### APROPOS -- searching

`:`

`doc`

and`:`

`more-doc`

text### ARRAYS -- an introduction to ACL2 arrays.

### BACKCHAIN-LIMIT -- limiting the effort expended on relieving hypotheses

### BIBLIOGRAPHY -- reports about ACL2

### BIND-FREE -- to bind free variables of a rewrite or linear rule

### BREAKS -- Common Lisp breaks

### CASE-SPLIT -- like force but immediately splits the top-level goal on the hypothesis

### CASE-SPLIT-LIMITATIONS -- a list of two ``numbers'' limiting the number of cases produced at once

### CHECK-SUM -- assigning ``often unique'' integers to files and objects

### CLAUSE-IDENTIFIER -- the internal form of a goal-spec

### COMMAND -- forms you type at the top-level, but...

### COMMAND-DESCRIPTOR -- an object describing a particular command typed by the user

### COMPUTED-HINTS -- computing advice to the theorem proving process

### CONSTRAINT -- restrictions on certain functions introduced in

`encapsulate`

events### COPYRIGHT -- ACL2 copyright, license, sponsorship

### COROLLARY -- the corollary formula of a rune

### CURRENT-PACKAGE -- the package used for reading and printing

### DEFAULT-BACKCHAIN-LIMIT -- specifying the backchain limit for a rule

### DEFAULT-DEFUN-MODE -- the default defun-mode of

`defun`

'd functions### DEFAULT-HINTS -- a list of hints added to every proof attempt

### DEFAULT-PRINT-PROMPT -- the default prompt printed by

`ld`

### DEFUN-MODE -- determines whether a function definition is a logical act

### DEFUN-MODE-CAVEAT -- functions with defun-mode of

`:`

`program`

considered unsound### DEFUNS -- an alternative to

`mutual-recursion`

### DISABLE-FORCING -- to disallow

`force`

d`case-split`

s### DISABLE-IMMEDIATE-FORCE-MODEP -- forced hypotheses are attacked immediately

### DISABLEDP -- determine whether a given name or rune is disabled

### E0-ORD-< -- the well-founded less-than relation on ordinals up to

`epsilon-0`

### E0-ORDINALP -- a recognizer for the ordinals up to epsilon-0

### EMBEDDED-EVENT-FORM -- forms that may be embedded in other events

### ENABLE-FORCING -- to allow

`force`

d`split`

s### ENABLE-IMMEDIATE-FORCE-MODEP -- forced hypotheses are attacked immediately

### ENTER-BOOT-STRAP-MODE -- The first millisecond of the Big Bang

### ESCAPE-TO-COMMON-LISP -- escaping to Common Lisp

### EVISCERATE-HIDE-TERMS -- to print

`(hide ...)`

as`<hidden>`

### EXECUTABLE-COUNTERPART -- a rule for computing the value of a function

### EXIT-BOOT-STRAP-MODE -- the end of pre-history

### EXTENDED-METAFUNCTIONS -- state and context sensitive metafunctions

### FAILED-FORCING -- how to deal with a proof failure in a forcing round

### FAILURE -- how to deal with a proof failure

### FIND-RULES-OF-RUNE -- find the rules named rune

### FORCE -- identity function used to force a hypothesis

### FORCING-ROUND -- a section of a proof dealing with forced assumptions

### GC$ -- invoke the garbage collector

### GENERALIZED-BOOLEANS -- potential soundness issues related to ACL2 predicates

### GOAL-SPEC -- to indicate where a hint is to be used

### GUARD -- restricting the domain of a function

### HIDE -- hide a term from the rewriter

### HINTS -- advice to the theorem proving process

### I-AM-HERE -- a convenient marker for use with

`rebuild`

### IMMEDIATE-FORCE-MODEP -- when executable counterpart is enabled,

### IN-PACKAGE -- select current package

### KEYWORD-COMMANDS -- how keyword commands are processed

### LD-ERROR-ACTION -- determines

`ld`

's response to an error### LD-ERROR-TRIPLES -- determines whether a form caused an error during

`ld`

### LD-EVISC-TUPLE -- determines whether

`ld`

suppresses details when printing### LD-KEYWORD-ALIASES -- allows the abbreviation of some keyword commands

### LD-POST-EVAL-PRINT -- determines whether and how

`ld`

prints the result of evaluation### LD-PRE-EVAL-FILTER -- determines which forms

`ld`

evaluates### LD-PRE-EVAL-PRINT -- determines whether

`ld`

prints the forms to be`eval`

'd### LD-PROMPT -- determines the prompt printed by

`ld`

### LD-QUERY-CONTROL-ALIST -- how to default answers to queries

### LD-REDEFINITION-ACTION -- to allow redefinition without undoing

### LD-SKIP-PROOFSP -- how carefully ACL2 processes your commands

### LD-VERBOSE -- determines whether

`ld`

prints ``ACL2 Loading ...''### LEMMA-INSTANCE -- an object denoting an instance of a theorem

### LINEAR-ARITHMETIC -- A description of the linear arithmetic decision procedure

### LOCAL-INCOMPATIBILITY -- when non-local events won't replay in isolation

### LOGICAL-NAME -- a name created by a logical event

### LOOP-STOPPER -- limit application of permutative rewrite rules

### LP -- the Common Lisp entry to ACL2

### MACRO-ARGS -- the formals list of a macro definition

### NAME -- syntactic rules on logical names

### NON-LINEAR-ARITHMETIC -- Non-linear Arithmetic

### NU-REWRITER -- rewriting

`NTH`

/`UPDATE-NTH`

expressions### OBDD -- ordered binary decision diagrams with rewriting

### OTF-FLG -- pushing all the initial subgoals

### PACKAGE-REINCARNATION-IMPORT-RESTRICTIONS -- re-defining undone

`defpkg`

s### PRINT-DOC-START-COLUMN -- printing the one-liner

### PROMPT -- the prompt printed by

`ld`

### PROOF-OF-WELL-FOUNDEDNESS -- a proof that

`e0-ord-<`

is well-founded on`e0-ordinalp`

s### PSEUDO-TERMP -- a predicate for recognizing term-like s-expressions

### REDEF -- a common way to set ld-redefinition-action

### REDEF! -- system hacker's redefinition command

### REDEFINED-NAMES -- to collect the names that have been redefined

### REDUNDANT-EVENTS -- allowing a name to be introduced ``twice''

### SAVING-AND-RESTORING -- saving and restoring your logical state

### SET-NON-LINEARP -- to turn on or off non-linear arithmetic reasoning

### SIGNATURE -- how to specify the arity of a constrained function

### SIMPLE --

`:`

`definition`

and`:`

`rewrite`

rules used in preprocessing### SPECIOUS-SIMPLIFICATION -- nonproductive proof steps

### STATE -- the von Neumannesque ACL2 state object

### SUBVERSIVE-INDUCTIONS -- why we restrict encapsulated recursive functions

### SUBVERSIVE-RECURSIONS -- why we restrict encapsulated recursive functions

### SYNTAX -- the syntax of ACL2 is that of Common Lisp

### SYNTAXP -- to attach a heuristic filter on a

`:`

`rewrite`

or`:`

`linear`

rule### TERM -- the three senses of well-formed ACL2 expressions or formulas

### TERM-ORDER -- the ordering relation on terms used by ACL2

### THE-METHOD -- how to find proofs

### TTREE -- tag trees

### TYPE-SET -- how type information is encoded in ACL2

### USING-COMPUTED-HINTS -- how to use computed hints

### USING-COMPUTED-HINTS-1 -- Driving Home the Basics

### USING-COMPUTED-HINTS-2 -- One Hint to Every Top-Level Goal in a Forcing Round

### USING-COMPUTED-HINTS-3 -- Hints as a Function of the Goal (not its Name)

### USING-COMPUTED-HINTS-4 -- Computing the Hints

### USING-COMPUTED-HINTS-5 -- Debugging Computed Hints

### USING-COMPUTED-HINTS-6 -- Using the computed-hint-replacement feature

### USING-COMPUTED-HINTS-7 -- Using the stable-under-simplificationp flag

### USING-COMPUTED-HINTS-8 -- Some Final Comments

### VERSION -- ACL2 Version Number

### WHY-BRR -- an explanation of why ACL2 has an explicit

`brr`

mode### WORLD -- ACL2 property lists and the ACL2 logical data base

### WORMHOLE --

`ld`

without`state`

-- a short-cut to a parallel universe### XARGS -- giving hints to

`defun`