MISCELLANEOUS

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 forced case-splits

• DISABLE-IMMEDIATE-FORCE-MODEP -- forced hypotheses are attacked immediately

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

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

• ENABLE-FORCING -- to allow forced splits

• 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,
  forced hypotheses are attacked immediately

• 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 defpkgs

• PRINT-DOC-START-COLUMN -- printing the one-liner

• PROMPT -- the prompt printed by ld

• PROOF-OF-WELL-FOUNDEDNESS -- a proof that o< is well-founded on o-ps

• 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''

• REWRITE-STACK-LIMIT -- limiting the stack depth of the ACL2 rewriter

• 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