This is documentation for ACL2 Version 3.0
Copyright (C) 2006  University of Texas at Austin

This program is free software; you can redistribute it and/or modify
it under the terms of the GNU General Public License as published by
the Free Software Foundation; either version 2 of the License, or
(at your option) any later version.

This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
GNU General Public License for more details.

You should have received a copy of the GNU General Public License
along with this program; if not, write to the Free Software
Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.

Written by:  Matt Kaufmann and J Strother Moore
Department of Computer Sciences
University of Texas at Austin
Austin, TX 78712-1188 U.S.A.

UNMONITOR    to stop monitoring a rule name

     Examples:
     (unmonitor '(:rewrite assoc-of-app))
     :unmonitor (:rewrite assoc-of-app)
     :unmonitor :all

     General Forms:
     (unmonitor rune)
     (unmonitor :all)

Here, rune is a rune that is currently among those with break points
installed.  This function removes the break.

Subtle point: Because you may want to unmonitor a "rune" that is no
longer a rune in the current ACL2 world, we don't actually check this
about rune.  Instead, we simply check that rune is a consp beginning
with a keywordp.  That way, you'll know you've made a mistake if you try
to :unmonitor binary-append instead of :unmonitor (:definition
binary-append), for example.

DOCUMENTATION    functions that display documentation at the terminal

This section explains the ACL2 online documentation system.  Thus, it
assumes that you are typing at the terminal, inside an ACL2 session.  If
you are reading this description in another setting (for example, on
paper), simply ignore the parts of this description that involve typing
at the terminal.

For an introduction to the ACL2 online documentation system, type :more
below.  Whenever the documentation system concludes with "(type :more
for more, :more! for the rest)" you may type :more to see the next block
of documentation.

Topics related to documentation are documented individually:

The ACL2 online documentation feature allows you to see extensive
documentation on many ACL2 functions and ideas.  You may use the
documentation facilities to document your own ACL2 functions and
theorems.

If there is some name you wish to know more about, then type

     ACL2 !>:doc name

in the top-level loop.  If the name is documented, a brief blurb will be
printed.  If the name is not documented, but is "similar" to some
documented names, they will be listed.  Otherwise, nil is returned.

Every name that is documented contains a one-line description, a few
notes, and some details.  :Doc will print the one-liner and the notes.
When :doc has finished it stops with the message "(type :more for more,
:more! for the rest)" to remind you that details are available.  If you
then type

     ACL2 !>:more

a block of the continued text will be printed, again concluding with
"(type :more for more, :more! for the rest)" if the text continues
further, or concluding with "*-" if the text has been exhausted.  By
continuing to type :more until exhausting the text you can read
successive blocks.  Alternatively, you can type :more! to get all the
remaining blocks.

If you want to get the details and don't want to see the elementary
stuff typed by :doc name, type:

     ACL2 !>:MORE-DOC name

We have documented not just function names but names of certain
important ideas too.  For example, see REWRITE and see
META to learn about :rewrite rules and :meta rules, respectively.  See
HINTS to learn about the structure of the :hints argument to the
prover.  The deflabel event (see DEFLABEL) is a way to introduce
a logical name for no reason other than to attach documentation to it;
also see DEFDOC.

How do you know what names are documented?  There is a documentation
data base which is querried with the :docs command.

The documentation data base is divided into sections.  The sections are
listed by

     ACL2 !>:docs *

Each section has a name, sect, and by typing

     ACL2 !>:docs sect

or equivalently

     ACL2 !>:doc sect

you will get an enumeration of the topics within that section.  Those
topics can be further explored by using :doc (and :more) on them.  In
fact the section name itself is just a documented name.  :more generally
gives an informal overview of the general subject of the section.

     ACL2 !>:docs **

will list all documented topics, by section.  This fills several pages
but might be a good place to start.

If you want documentation on some topic, but none of our names or brief
descriptions seem to deal with that topic, you can invoke a command to
search the text in the data base for a given string.  This is like the
GNU Emacs "apropos" command.

     ACL2 !>:docs "functional inst"

will list every documented topic whose :doc or :more-doc text includes
the substring "functional inst", where case and the exact number of
spaces are irrelevant.

If you want documentation on an ACL2 function or macro and the
documentation data base does not contain any entries for it, there are
still several alternatives.

     ACL2 !>:args fn

will print the arguments and some other relevant information about the
named function or macro.  This information is all gleaned from the
definition (not from the documentation data base) and hence this is a
definitive way to determine if fn is defined as a function or macro.

You might also want to type:

     ACL2 !>:pc fn

which will print the command which introduced fn.  You should see
COMMAND-DESCRIPTOR for details on the kinds of input you can give the
:pc command.

The entire ACL2 documentation data base is user extensible.  That is, if
you document your function definitions or theorems, then that
documentation is made available via the data base and its query
commands.

The implementation of our online documentation system makes use of
Common Lisp's "documentation strings." While Common Lisp permits a
documentation string to be attached to any defined concept, Common Lisp
assigns no interpretation to these strings.  ACL2 attaches special
significance to documentation strings that begin with the characters
":doc-section".  When such a documentation string is seen, it is stored
in the data base and may be displayed via :doc, :more, :docs, etc.  Such
documentation strings must follow rigid syntactic rules to permit their
processing by our commands.  These are spelled out elsewhere; see
DOC-STRING.

A description of the structure of the documentation data base may also
be found; see DOC-STRING.

*TERMINAL-MARKUP-TABLE*    a markup table used for printing to the terminal

The value of the ACL2 constant *terminal-markup-table* is an association
list pairing markup keys with strings, to be used for printing to the
terminal.  See MARKUP for a description of the ACL2 markup
language.

The entries in *terminal-markup-table* are of the form

     (key . fmt-string)

where key is one of the doc-string tilde directives (see
MARKUP), and fmt-string is a string as expected by the ACL2 printing
function fmt.  The system arranges that for any arg, when an expression
~key[arg] is encountered by the documentation printer, fmt will print
fmt-string in the association list where #\a is bound to arg and #\A is
bound to the result of applying the function string-upcase to arg.

It is possible to implement tools in ACL2 for printing documentation to
other than the terminal.  In fact, such tools exist for Texinfo and for
HTML.  For now, discussion of this capability is beyond the scope of the
present topic.

ARGS    args, guard, type, constraint, etc., of a function symbol

     Example:
     :args assoc-eq

Args takes one argument, a symbol which must be the name of a function
or macro, and prints out the formal parameters, the guard expression,
the output signature, the deduced type, the constraint (if any), and
whether documentation about the symbol is available via :doc.

DOC    brief documentation (type :doc name)

NOTE: The :doc command only makes sense at the terminal.  Furthermore it
only works at the terminal when a "full-size" image has been built.
Most users will probably access the ACL2 documentation in other ways, as
explained in the file "doc/README" that comes with the ACL2
distribution.

     Examples:
     ACL2 !>:doc DEFTHM          ; print documentation of DEFTHM
     ACL2 !>:doc logical-name    ; print documentation of LOGICAL-NAME
     ACL2 !>:doc "MY-PKG"      ; print documentation of "MY-PKG"

     Related Topics:
     :more                      ; continues last :doc or :more-doc text
     :more-doc name             ; prints more documentation for name
     :docs **                   ; lists all documented symbols
     :docs "compil"             ; documented symbols apropos "compil"
     :DOC documentation         ; describes how documentation works

     General Form:
     ACL2>:doc logical-name

where logical-name is a logical name (see LOGICAL-NAME) for
which you hope there is documentation.  Chances are there is no
documentation at the moment, but we are working on adding documentation
strings for all the user level ACL2 functions.

For a general discussion of our treatment of documentation strings, see
DOCUMENTATION.

This is the first cut at online documentation.  Users can be
particularly helpful by sending mail on the inadequacies of the system.
Address it just to Moore and put Documentation in the subject line.
There are several things that trouble me about what I've done here.

First, many concepts aren't documented.  Ultimately, I'd like to
.  document (a) every CLTL primitive (e.g., case and coerce) and (b)
every ACL2 extension (e.g., aref1 and getprop).  But so far I have
focussed on documenting (c) the ACL2 system primitives (e.g., defthm and
what hints look like).  My priorities are (c), then (b), and then (a),
following the philosophy that the most unstable features should get
online documentation in these early releases.  Having gotten the basic
documentation in place, I'll document new things as they are added, and
in response to your pleas I'll try to add documentation to old things
that are widely regarded as important.

Second, I worry that the existing documentation is unhelpful because it
provides too much or too little detail, or it provides the detail too
far away from where it is needed.  Please be on the lookout for this.
Did you get what you needed when you appealed to :doc or :more-doc?  If
not, what was it you needed?  Would more cross-references help?  Did you
get lost in maze of cross-references?

DOC!    all the documentation for a name (type :doc! name)

NOTE: The :doc! command only makes sense at the terminal.

     Examples:
     ACL2 !>:doc! defthm
     ACL2 !>:doc! certificate

This command is like :doc name followed by :more!.  It prints all the
documentation of name.

DOC-STRING    formatted documentation strings

     Examples:
     ":Doc-Section name
     one-liner~/notes~/details"

     ":Doc-Section name
     one-liner~/
     notes~/
     details~/
     :cite old-name1
     :cited-by old-name2"

Use (get-doc-string 'name state) to see other examples.

Documentation strings not beginning with ":Doc-Section" (case is
irrelevant) are ignored.  See MARKUP for how to supply
formatting information (such as fonts and displayed text) in
documentation strings.

ACL2 attaches special importance to documentation strings beginning with
the header ":Doc-Section" (or any variant thereof obtained by changing
case).  Any documentation string that does not begin with such a header
is considered unformatted and is ignored.  For the rest of this
discussion, we use the phrase "documentation string" as though it read
"formatted documentation string."

Documentation strings are always processed in the context of some
symbol, name, being defined.  (Indeed, if an event defines no symbol,
e.g., verify-guards or in-theory, then it is not permitted to have a
formatted documentation string.)  The string will be associated with
name in the "documentation data base." The data base is divided into
"sections" and each section is named by a symbol.  Among the sections
are events, documentation, history, other, and miscellaneous.  A
complete list of the sections may be obtained by typing :docs * at the
terminal.  You can create new sections.  The main purpose of sections is
simply to partition the large set of names into smaller subsets whose
contents can be enumerated separately.  The idea is that the user may
remember (or recognize) the relevant section name and then read its
contents to find interesting items.

Within a section are "documentation tuples" which associate with each
documented name its documentation string and a list of related
documented names, called the "related names" of the name.  When :doc
prints the documentation for name, it always lists the related names.

When a formatted documentation string is submitted with the defining
event of some name, the section name and an initial set of related names
are parsed from the string.  In addition, the formatted string contains
various "levels" of detail that are printed out at different times.
Finally, it is possible for a string to cause the newly documented name
to be added to the related names of any previously documented name.
Thus, as new names are introduced they can be grouped with old ones.

The general form of an ACL2 formatted documentation string is

     ":DOC-SECTION <section-name>
       <one-liner>~/
       <notes>~/
       <details>~/
       :CITE <n1>
       ...
       :CITE <nn>
       :CITED-BY <m1>
       ...
       :CITED-BY <mm>"

Before we explain this, let it be noted that (get-doc-string name state)
will return the documentation string associated with name in the
documentation data base.  You may want to call get-doc-string on 'pe and
'union-theories just to see some concrete documentation strings.  This
documentation string, which is rather long, is under 'doc-string.

A formatted documentation string has five parts: the header and
section-name (terminating in the first #\Newline), the <one-liner>,
<notes>, and <details> (each terminating in a tilde-slash ("~/") pair),
and a citation part.  These five parts are parsed into six components.
<section-name> is read as the name of a symbol, section-name.
<one-liner>, <notes>, and <details> are arbitrary sequences of
characters (ignoring initial white space and not including the
tilde-slash pairs which terminate them).  The <ni> are read as symbols
and assembled into a list called the "cite" symbols.  The <mi> are read
as symbols and assembled into a list called the "cited-by" symbols.  See
the warning below regarding the hackish nature of our symbol reader.

Section-name must either be a previously documented symbol or else be
name, the symbol being documented.  To open a new section of the data
base, named section-name, you should define the logical name
section-name (as by deflabel or any other event; also see
DEFDOC) and attach to it a documentation string for section
section-name.  You might wish to print out the documentation string we
use for some of our section names, e.g., (get-doc-string 'events state).
By forcing section names to be documented symbols, we permit sections
themselves to have one line descriptions and discussions, presented by
the standard documentation facilities like the facilities :doc and
:more-doc that may be used at the terminal.

Each of the ni's and mi's must be previously documented symbols.

Both <one-liner> and <details> must be non-empty, i.e., must contain
some non-whitespace characters.  <notes> may be empty.  The :cites and
:cited-bys pairs may be intermingled and may be separated by either
newlines or spaces.  The citation part may be empty.  When the citation
part is empty, the tilde-slash pair terminating the <details> part may
be omitted.  Thus, the simplest form of a formatted documentation string
is:

     ":Doc-Section <section-name>
      <one-liner>~/~/
      <details>"

Since white space at the front of <one-liner>, <notes> and <details> is
ignored, we often precede those parts by #\Newlines to make the strings
easier to read in our source files.  We also typically indent all of the
text in the string by starting each line with a few spaces.  (The Emacs
commands for formatting Lisp get confused if you have arbitrary
characters on the left margin.)  We assume that every line in
<one-liner>, <notes>, and <details> starts with at least as many spaces
as <one-liner> does, i.e., we assume they are all indented the same
amount (or more).  Let d be the number of spaces separating <one-liner>
from the #\Newline preceding it.  When the various parts are printed, we
"de-indent" by stripping out the first d spaces following each
#\Newline.

However, we find that when documentation is printed flush against the
left margin it is difficult to distinguish the documentation text from
previous output.  We therefore prefix each line we print by a special
pad of characters.  By default, this pad is "| " so that documentation
text has a vertical bar running down the left margin.  But the pad is
just the value of the global variable doc-prefix and you may assign it
any string you wish.

To add such a string to the data base under the symbol name we make a
new entry in the section-name section of the data base.  The entry
associates name with the string and uses the string's cites list as the
initial value of the related names field.  In addition, we add name to
the related names field of each of the names listed in the string's
cited-by list.  We also add name to the related names field of its
section-name.  Observe that the cites list in a string is only the
initial value of the related names of the names.  Future documentation
strings may add to it via :cited-by or :doc-section.  Indeed, this is
generally the case.  We discuss this further below.

When a brief description of name is required (as by :docs **), name and
<one-liner> are printed.  <one-liner> is usually printed starting in
column 15 (however see PRINT-DOC-START-COLUMN).  Despite its
name, <one-liner> need not be one line.  It usually is one line,
however.

When you type :doc name at the terminal, the first response will be to
print name and <one-liner>.  Then :doc prints <notes>, if any.  Then, if
name is the name of a section, it prints the <one-liner>s for each of
its related names.  For example, try :doc events.  If name is not a
section name but does have some related names, they are merely listed
but not explained.  Try :doc theory-functions.  :more-doc name prints
<details>.

Our style is to let each new concept add itself to the related names of
old concepts.  To do otherwise increases the chances that documentation
gets outdated because one often forgets to update supposedly complete
lists of the relevant topics when new topics are invented.  For example,
:doc theory-functions lists each available theory function.  But
get-doc-string of 'theory-functions just shows a few examples and has an
empty cites list.  From where do we get the names of the theory
functions listed by :doc?  The answer is that each theory function has
its own documentation string and those strings each specify :cited-by
theory-functions.  See for example get-doc-string of 'union-theories.
So by the time the entire system is assembled, the related names of
'theory-functions contains all the (documented) theory functions.  This
makes it easy to add new theory functions without changing the general
discussion in 'theory-functions.

When an event or command form is printed, as by :pe or :pc, that
contains a formatted documentation string, we do not print the actual
documentation string (since they are usually large and distracting).
Instead we print the string:

       "Documentation available via :doc"

inviting you to use :doc and :more-doc (or get-doc-string) if you wish
to see the documentation at the terminal.

*Warning on Reading Symbols from Strings:* When we read a symbol, such
as the section-symbol, from a documentation string, we use a quick and
dirty imitation of the much more powerful CLTL read program.  In
particular, we scan past any whitespace, collect all the characters we
see until we get to more whitespace or the end of the string, convert
the characters to upper case, make a string out of them, and intern that
string.  Thus, if you typed ":Doc-Section 123 ..." we would read the 123
as the symbol |123|.  Observe that special characters, such as
parentheses and escape characters, are not afforded their usual
reverence by our hack.  Furthermore, the question arises: in which
package do we intern the symbol?  The answer is, usually, the package
containing the name being defined.  I.e., if you are documenting
my-pkg::name and you attach a documentation string that begins
":Doc-Section: Machines ..." then the section-symbol will be
my-pkg::machines.  We recognize two special cases. If the first
character read is a colon, we use the keyword package.  If the first
five characters read are acl2:: then we intern in the "ACL2" package.
Our own section names, e.g., events, are in the "ACL2" package.

In a related area, when you ask for the documentation of a name, e.g.,
when you type :doc name at the terminal, that name is read with the full
ACL2 reader, not the hack just described.  That name is read into the
current package.  Thus, if you are operating in-package "MY-PKG" and
type :doc events, what is read is my-pkg::events.  The data base may not
contain an entry for this symbol.  Before reporting that no
documentation exists, we try acl2::events.

One last note: defpkg permits a formatted documentation string, which is
associated in the data base with the name of the package.  But the name
of the package is a string, not a symbol.  It is permitted to access the
documentation of a string (i.e., package name).  But there are no
facilities for getting such a stringp name into the related names of
another name nor of making such stringp names be section names.  That is
because we always read symbols from strings and never read strings from
strings.  I.e., if you did write "Doc-Section \"MY-PKG\" ..." it would
read in as a weird symbol.

DOCS    available documentation topics (by section)

NOTE: The :docs command only makes sense at the terminal.

When the :docs command is given a stringp argument it searches the text
produced by :doc and :more-doc and lists all the documented topics whose
text contains the given string.  For purposes of this string matching we
ignore distinctions of case and the amount and kind (but not presence)
of white space.  We also treat hyphen as whitespace.

However, the following examples show how :docs can be used on other than
string patterns.

     Examples:
     ACL2 !>:docs *           ; lists documentation sections
     ACL2 !>:docs **          ; lists all documented topics within all sections
     ACL2 !>:docs events      ; lists all topics in section EVENTS
     ACL2 !>:docs "compil"    ; lists topics "apropos"

The data base of formatted documentation strings is structured into
sections.  Within a section are topics.  Each topic has a one-liner,
some notes, and some detailed discussions.  The :docs command provides a
view of the entire data base.

:docs takes one argument, as described below:

     arg               effect

     *                 list all section headings in the data base
     **                list all section headings and all topics within
                       each section
     name              list all topics in the section named name (where
                       name is some symbol other than * and **).  This
                       is always the same as :doc name.
     pattern           list all topics whose :doc or :more-doc text
                       mentions the string pattern.  For purposes of this
                       string matching we ignore distinctions of case and
                       the amount and kind (but not presence) of white
                       space.  We also treat hyphen as whitespace.

HELP    brief survey of ACL2 features

     Example:
     ACL2 !>:help

See LP for general information about the top-level command
environment for ACL2.

MARKUP    the markup language for ACL2 documentation strings

ACL2 documentation strings make special use of the tilde character (~).
In particular, we describe here a "markup language" for which the tilde
character plays a special role.  The markup language is valuable if you
want to write documentation that is to be displayed outside your ACL2
session.  If you are not writing such documentation, and if also you do
not use the character `~', then there is no need to read on.

Three uses of the tilde character (~) in documentation strings are as
follows.  Below we explain the uses that constitute the ACL2 markup
language.

     ~/

     Indicates the end of a documentation *section*; see
     DOC-STRING.

     ~~

     Indicates the literal insertion of a tilde character (~).

     ~]

     This directive in a documentation string is effective only during
     the processing of part 2, the details (see DOC-STRING), and
     controls how much is shown on each round of :more processing when
     printing to the terminal.  If the system is not doing :more
     processing, then it acts as though the ~] is not present.
     Otherwise, the system put out a newline and halts documentation
     printing on the present topic, which can be resumed if the user
     types :more at the terminal.

The other uses of the tilde character are of the following form.

       ~key[arg]

Before launching into an explanation of how this works in detail, let us
consider some small examples.

Here is a word that is code:

       ~c[function-name].

Here is a phrase with an "emphasized" word, "not":

       Do ~em[not] do that.

Here is the same phrase, but where "not" receives stronger emphasis
(presumably boldface in a printed version):

       Do ~st[not] do that.

Here is a passage that is set off as a display, in a fixed-width font:

       ~bv[]
       This passage has been set off as "verbatim".
       The present line starts just after a line break.  Normally, printed
       text is formatted, but inside ~bv[]...~ev[], line breaks are taken
       literally.
       ~ev[]

In general, the idea is to provide a "markup language" that can be
reasonably interpreted not only at the terminal (via :doc), but also via
translators into other languages.  In fact, translators have been
written into Texinfo and HTML.

Let us turn to a more systematic consideration of how to mark text in
documentation strings using expressions of the form ~key[arg], which we
will call "doc-string tilde directives."  The idea is that key informs
the documentation printer (which could be the terminal, a hardcopy
printer, or some hypertext tool) about the "style" used to display arg.
The intention is that each such printer should do the best it can.  For
example, we have seen above that ~em[arg] tells the printer to emphasize
arg if possible, using an appropriate display to indicate emphasis
(italics, or perhaps surrounding arg with some character like _, or
...).  For another example, the directive for bold font, ~b[arg], says
that printed text for arg should be in bold if possible, but if there is
no bold font available (such as at the terminal), then the argument
should be printed in some other reasonable manner (for example, as
ordinary text).  The key part is case-insensitive; for example, you can
use ~BV[] or ~Bv[] or ~bV[] in place of ~bv[].

Every form below may have any string as the argument (inside [..]), as
long as it does not contain a newline (more on that below).  However,
when an argument does not make much sense to us, we show it below as the
empty string, e.g., "~bv[]" rather than "~bv[arg]".

     ~-[]      Print the equivalent of a dash

     ~b[arg]   Print the argument in bold font, if available

     ~bid[arg]   "Begin implementation dependent" -- Ignores argument at
               terminal.

     ~bf[]     Begin formatted text (respecting spaces and line breaks),
               but in ordinary font (rather than, say, fixed-width font)
               if possible

     ~bq[]     Begin quotation (indented text, if possible)

     ~bv[]     Begin verbatim (print in fixed-width font, respecting
               spaces and line breaks)

     ~c[arg]   Print arg as "code", such as in a fixed-width font

     ~ef[]     End format; balances ~bf[]

     ~eid[arg]   "End implementation dependent" -- Ignores argument at
               terminal.

     ~em[arg]  Emphasize arg, perhaps using italics

     ~eq[]     End quotation; balances ~bq[]

     ~ev[]     End verbatim; balances ~bv[]

     ~i[arg]   Print arg in italics font

     ~id[arg]   "Implementation dependent" -- Ignores argument at
               terminal.

     ~il[arg]  Print argument as is, but make it a link (for true
               hypertext environments)

     ~ilc[arg] Same as ~il[arg], except that arg should be printed as
               with ~c[arg]

     ~l[arg]   Ordinary link; prints as "See :DOC arg" at the terminal
               (but also see ~pl below, which puts "see" in lower case)

     ~nl[]     Print a newline

     ~par[]    Paragraph mark, of no significance at the terminal
               (can be safely ignored; see also notes below)

     ~pl[arg]  Parenthetical link (borrowing from Texinfo):  same as
               ~l[arg], except that "see" is in lower case.  This is
               typically used at other than the beginning of a sentence.

     ~sc[arg]  Print arg in (small, if possible) capital letters

     ~st[arg]  Strongly emphasize arg, perhaps using a bold font

     ~t[arg]   Typewriter font; similar to ~c[arg], but leaves less
               doubt about the font that will be used.

     ~terminal[arg]  Terminal only; arg is to be ignored except when
               reading documentation at the terminal, using :DOC.

*Style notes and further details*

It is not a good idea to put doc-string tilde directives inside verbatim
environments, ~bv[] ... ~ev[].

Do not nest doc-string tilde directives; that is, do not write

       The ~c[~il[append] function ...

but note that the "equivalent" expression

       The ~ilc[append] function ...

is fine.  The following phrase is also acceptable:

       ~bf[]This is
       ~em[formatted] text.
       ~ef[]

because the nesting is only conceptual, not literal.

We recommend that for displayed text, ~bv[] and ~ev[] should usually
each be on lines by themselves.  That way, printed text may be less
encumbered with excessive blank lines.  Here is an example.

       Here is some normal text.  Now start a display:
       ~bv[]
         2 + 2 = 4
       ~ev[]
       And here is the end of that paragraph.

       Here is the start of the next paragraph.

The analogous consideration applies to ~bf[] and ~ef[] as well as ~bq[]
and ~eq[].

You may "quote" characters inside the arg part of ~key[arg], by
preceding them with ~.  This is, in fact, the only legal way to use a
newline character or a right bracket (]) inside the argument to a
doc-string tilde directive.

Write your documentation strings without hyphens.  Otherwise, you may
find your text printed on paper (via TeX, for example) like this ---

       Here is a hyphe- nated word.

even if what you had in mind was:

       Here is a hyphe-
       nated word.

When you want to use a dash (as opposed to a hyphen), consider using
~-[], which is intended to be interpreted as a "dash."  For example:

       This sentence ~-[] which is broken with dashes ~-[] is boring.

would be written to the terminal (using :doc) by replacing ~-[] with two
hyphen characters, but would presumably be printed on paper with a dash.

Be careful to balance the "begin" and "end" pairs, such as ~bv[] and
~ev[].  Also, do not use two "begin" directives (~bf[], ~bq[], or ~bv[])
without an intervening "end" directive.  It is permissible (and perhaps
this is not surprising) to use the doc-string part separator ~/ while
between such a begin-end pair.

Because of a bug in texinfo (as of this writing), you may wish to
avoid beginning a line with (any number of spaces followed by) the
- character or ~-[].

The "paragraph" directive, ~par[], is rarely if ever used.  There is a
low-level capability, not presently documented, that interprets two
successive newlines as though they were ~par[].  This is useful for the
HTML driver.  For further details, see the authors of ACL2.

Emacs code is available for manipulating documentation strings that
contain doc-string tilde-directives (for example, for doing a reasonable
job filling such documentation strings).  See the authors if you are
interested.

We tend to use ~em[arg] for "section headers," such as "Style notes and
further details" above.  We tend to use ~st[arg] for emphasis of words
inside text.  This division seems to work well for our Texinfo driver.
Note that ~st[arg] causes arg to be printed in upper-case at the
terminal (using :doc), while ~em[arg] causes arg to be printed at the
terminal as though arg were not marked for emphasis.

Our Texinfo and HTML drivers both take advantage of capabilities for
indicating which characters need to be "escaped," and how.  Unless you
intend to write your own driver, you probably do not need to know more
about this issue; otherwise, contact the ACL2 authors.  We should
probably mention, however, that Texinfo makes the following requirement:
when using ~l[arg], where arg contains one of the special characters @,
{, or }, you must immediately follow this use with a period or comma.
Also, the Emacs "info" documentation that we generate by using our
Texinfo driver has the property that in node names, : has been replaced
by | (because of quirks in info); so for example, the "proof-checker"
simplification command, s, is documented under acl2-pc||s rather than
under acl2-pc::s.

We have tried to keep this markup language fairly simple; in particular,
there is no way to refer to a link by other than the actual name.  So
for example, when we want to make :doc an invisible link in "code" font,
we write the following form, which indicates that : should be in that
font and then doc should both be in that font and be an invisible link.

       ~c[:]~ilc[doc]

MORE    your response to :doc or :more's "(type :more...)"

NOTE: The command :more only makes sense at the terminal.

     Example:
     ACL2 !>:more

will continue printing whatever documentation was started by :doc or
:more-doc.

When you type :doc name, for some documented name, the system responds
by typing the one-liner and the notes sections of the documentation for
name.  It then types "(type :more for more, :more! for the rest)".  If
you then type

     ACL2 !>:more

the system will start to print the details section of name.  The same
thing could be achieved by typing :more-doc name, but that requires you
to type name again.

Similarly, if you have typed :more-doc name, the system will print the
first "block" of the details section and then print "(type :more for
more, :more! for the rest)".  Typing :more at that point will cause the
next block of the details section to be printed.  Eventually :more will
conclude by printing "*-" which is the indicator that the text has been
exhausted.

What is a "block" of text?  :More looks for the end of a paragraph (two
adjacent newlines) after printing n lines.  If it doesn't find one
before it has printed k lines, it just stops there.  N and k here are
the values of the two state global variables 'more-doc-min-lines and
'more-doc-max-lines.  You may use @ and assign to inspect and set these
variables, e.g., (@ more-doc-max-lines) will return the current maximum
number of lines printed by :more and (assign more-doc-max-lines 19) will
set it to 19.  On terminals having only 24 lines, we find min and max
settings of 12 and 19 the most pleasant.

If you want :more to print all of the details instead of feeding them to
you one block at a time, type :more! instead.

MORE!    another response to "(type :more for more, :more! for the rest)"

NOTE: The command :more! only makes sense at the terminal.

     Example:
     ACL2 !>:more!

will print all of the remaining documentation started by the last :doc
or :more-doc.

See MORE for some background.  Typing :more! will print all
remaining blocks of documentation.

:More! is like :more except that it prints all the text at once.  For
example, if you type :doc name you will see some text followed by "(type
:more for more, :more! for the rest)".  If you then type simply :more!
you will see all of the details, while if you type :more you will be fed
the next block of details.

MORE-DOC    a continuation of the :doc documentation

NOTE: The :more-doc command only makes sense at the terminal.

     Examples:
     ACL2 !>:more-doc DEFTHM
     ACL2 !>:more-doc logical-name

Often it is assumed in the text provided by :more-doc name that you have
read the text provided by :doc name.

:More-doc just continues spewing out at you the documentation string
provided with a definition.  If the user has done his job, :doc will
probably remind you of the basics and :more-doc, if read after :doc,
will address obscure details that are nevertheless worth noting.

When :more-doc types "(type :more for more, :more! for the rest)" you
can get the next block of the continuation by typing :more or all of the
remaining blocks by typing :more!.  See MORE.

NQTHM-TO-ACL2    ACL2 analogues of Nqthm functions and commands

     Example Forms:
     :nqthm-to-acl2 prove-lemma   ; Display ACL2 topic(s) and/or print
                                  ; information corresponding to Nqthm
                                  ; PROVE-LEMMA command.
     (nqthm-to-acl2 'prove-lemma) ; Same as above.

     General Form:
     (nqthm-to-acl2 name)

where name is a notion documented for Nqthm: either a function in the
Nqthm logic, or a command.  If there is corresponding information
available for ACL2, it will be printed in response to this command.
This information is not intended to be completely precise, but rather,
is intended to help those familiar with Nqthm to make the transition to
ACL2.

We close with two tables that contain all the information used by this
nqthm-to-acl2 command.  The first shows the correspondence between
functions in the Nqthm logic and corresponding ACL2 functions (when
possible); the second is similar, but for commands rather than
functions.

     Nqthm functions  -->     ACL2
     ----------------------------------------
     ADD1          -->  1+
     ADD-TO-SET    -->  ADD-TO-SET-EQUAL and ADD-TO-SET-EQ
     AND           -->  AND
     APPEND        -->  APPEND and BINARY-APPEND
     APPLY-SUBR    -->  No correspondent, but see the documentation for
                        DEFEVALUATOR and META.
     APPLY$        -->  No correspondent, but see the documentation for
                        DEFEVALUATOR and META.
     ASSOC         -->  ASSOC-EQUAL, ASSOC and ASSOC-EQ
     BODY          -->  No correspondent, but see the documentation for
                        DEFEVALUATOR and META.
     CAR           -->  CAR
     CDR           -->  CDR
     CONS          -->  CONS
     COUNT         -->  ACL2-COUNT
     DIFFERENCE    -->  -
     EQUAL         -->  EQUAL, EQ, EQL and =
     EVAL$         -->  No correspondent, but see the documentation for
                        DEFEVALUATOR and META.
     FALSE         -->  Nqthm's F corresponds to the ACL2 symbol NIL.
     FALSEP        -->  NOT and NULL
     FORMALS       -->  No correspondent, but see the documentation for
                        DEFEVALUATOR and META.
     GEQ           -->  >=
     GREATERP      -->  >
     IDENTITY      -->  IDENTITY
     IF            -->  IF
     IFF           -->  IFF
     IMPLIES       -->  IMPLIES
     LEQ           -->  <=
     LESSP         -->  <
     LISTP         -->  CONSP
     LITATOM       -->  SYMBOLP
     MAX           -->  MAX
     MEMBER        -->  MEMBER-EQUAL, MEMBER and MEMBER-EQ
     MINUS         -->  - and UNARY--
     NEGATIVEP     -->  MINUSP
     NEGATIVE-GUTS -->  ABS
     NLISTP        -->  ATOM
     NOT           -->  NOT
     NUMBERP       -->  ACL2-NUMBERP, INTEGERP and RATIONALP
     OR            -->  OR
     ORDINALP      -->  O-P
     ORD-LESSP     -->  O<
     PACK          -->  See intern and coerce.
     PAIRLIST      -->  PAIRLIS$
     PLUS          -->  + and BINARY-+
     QUOTIENT      -->  /
     REMAINDER     -->  REM and MOD
     STRIP-CARS    -->  STRIP-CARS
     SUB1          -->  1-
     TIMES         -->  * and BINARY-*
     TRUE          -->  The symbol T.
     UNION         -->  UNION-EQUAL and UNION-EQ
     UNPACK        -->  See symbol-name and coerce.
     V&C$          -->  No correspondent, but see the documentation for
                        DEFEVALUATOR and META.
     V&C-APPLY$    -->  No correspondent, but see the documentation for
                        DEFEVALUATOR and META.
     ZERO          -->  The number 0.
     ZEROP         -->  ZP

     ========================================

     Nqthm commands   -->     ACL2
     ----------------------------------------
     ACCUMULATED-PERSISTENCE
                   -->  ACCUMULATED-PERSISTENCE
     ADD-AXIOM     -->  DEFAXIOM
     ADD-SHELL     -->  There is no shell principle in ACL2.
     AXIOM         -->  DEFAXIOM
     BACKQUOTE-SETTING
                   -->  Backquote is supported in ACL2, but not
                        currently documented.
     BOOT-STRAP    -->  GROUND-ZERO
     BREAK-LEMMA   -->  MONITOR
     BREAK-REWRITE -->  BREAK-REWRITE
     CH            -->  PBT
                        See also :DOC history.
     CHRONOLOGY    -->  PBT
                        See also :DOC history.
     COMMENT       -->  DEFLABEL
     COMPILE-UNCOMPILED-DEFNS
                   -->  COMP
     CONSTRAIN     -->  See :DOC encapsulate and :DOC local.
     DATA-BASE     -->  Perhaps the closest ACL2 analogue of DATA-BASE
                        is PROPS.  But see :DOC history for a collection
                        of commands for querying the ACL2 database
                        ("world").  Note that the notions of
                        supporters and dependents are not supported in
                        ACL2.
     DCL           -->  DEFSTUB
     DEFN          -->  DEFUN and DEFMACRO
     DEFTHEORY     -->  DEFTHEORY
     DISABLE       -->  DISABLE
     DISABLE-THEORY
                   -->  See :DOC theories.  The Nqthm command
                        (DISABLE-THEORY FOO) corresponds roughly to the
                        ACL2 command
                        (in-theory (set-difference-theories
                                     (current-theory :here)
                                     (theory 'foo))).
     DO-EVENTS     -->  LD
     DO-FILE       -->  LD
     ELIM          -->  ELIM
     ENABLE        -->  ENABLE
     ENABLE-THEORY -->  See :DOC theories.  The Nqthm command
                        (ENABLE-THEORY FOO) corresponds roughly to the
                        ACL2 command
                        (in-theory (union-theories
                                     (theory 'foo)
                                     (current-theory :here))).
     EVENTS-SINCE  -->  PBT
     FUNCTIONALLY-INSTANTIATE
                   -->  ACL2 provides a form of the :USE hint that
                        corresponds roughly to the
                        FUNCTIONALLY-INSTANTIATE event of Nqthm. See
                        :DOC lemma-instance.
     GENERALIZE    -->  GENERALIZE
     HINTS         -->  HINTS
     LEMMA         -->  DEFTHM
     MAINTAIN-REWRITE-PATH
                   -->  BRR
     MAKE-LIB      -->  There is no direct analogue of Nqthm's notion of
                        "library."  See :DOC books for a description
                        of ACL2's mechanism for creating and saving
                        collections of events.
     META          -->  META
     NAMES         -->  NAME
     NOTE-LIB      -->  INCLUDE-BOOK
     PPE           -->  PE
     PROVE         -->  THM
     PROVEALL      -->  See :DOC ld and :DOC certify-book.  The latter
                        corresponds to Nqthm's PROVE-FILE,which may be
                        what you're interested in,really.
     PROVE-FILE    -->  CERTIFY-BOOK
     PROVE-FILE-OUT
                   -->  CERTIFY-BOOK
     PROVE-LEMMA   -->  DEFTHM
                        See also :DOC hints.
     R-LOOP        -->  The top-level ACL2 loop is an evaluation loop as
                        well, so no analogue of R-LOOP is necessary.
     REWRITE       -->  REWRITE
     RULE-CLASSES  -->  RULE-CLASSES
     SET-STATUS    -->  IN-THEORY
     SKIM-FILE     -->  LD-SKIP-PROOFSP
     TOGGLE        -->  IN-THEORY
     TOGGLE-DEFINED-FUNCTIONS
                   -->  EXECUTABLE-COUNTERPART-THEORY
     TRANSLATE     -->  TRANS and TRANS1
     UBT           -->  UBT and U
     UNBREAK-LEMMA -->  UNMONITOR
     UNDO-BACK-THROUGH
                   -->  UBT
     UNDO-NAME     -->  See :DOC ubt.  There is no way to undo names in
                        ACL2 without undoing back through such names.
                        However, see :DOC ld-skip-proofsp for
                        information about how to quickly recover the
                        state.

EVENTS    functions that extend the logic

Any extension of the syntax of ACL2 (i.e., the definition of a new
constant or macro), the axioms (i.e., the definition of a function), or
the rule data base (i.e., the proof of a theorem), constitutes a logical
"event." Events change the ACL2 logical world (see WORLD).
Indeed, the only way to change the ACL2 world is via the successful
evaluation of an event function.  Every time the world is changed by an
event, a landmark is left on the world and it is thus possible to
identify the world "as of" the evaluation of a given event.  An event
may introduce new logical names.  Some events introduce no new names
(e.g., verify-guards), some introduce exactly one (e.g., defmacro and
defthm), and some may introduce many (e.g., encapsulate ).