I gave an acl2-doc talk in Vienna 2014, but there are new features I
want to discuss today and besides, I want to evangelize a bit because
I think acl2-doc is a really useful tool for ACL2 users who work
inside Emacs.  I'll demo the / and W commands (documented at the end,
below) after reviewing the basics of acl2-doc.

NOTE: I made a video in November 2015 that introduces acl2-doc.  It's
changed some since then (in particular, with the addition of / and W),
but maybe you'll find it helpful:

http://www.cs.utexas.edu/users/kaufmann/demos/acl2-doc.movx

Today I'll start with h -- commands fit on a screen -- and t.  I'll
just go through the commands, perhaps illustrating with REWRITE.

Demo switching manuals, using my UT connection to show Kestrel manuals
too.

To demo / and W, I'll first remove TAGS-acl2-doc, then try / and W,
and follow directions, to build the tags table (which is built
automatically when you build the manual; see
xdoc::save-rendered-event
in books/doc/top.lisp).

make TAGS-acl2-doc

Example:

g RTL::NORMAL_ENCODINGS

and then put cursor on <normp> and hit
  meta-3 control-t /
three times to get to the definition in reps.lisp.

From :DOC acl2-doc:

    /             acl2-doc-definition
    (also control-t /)
       Find an ACL2 definition (in analogy to built-in Emacs command meta-.).
       With numeric prefix argument, find the next matching definition;
       otherwise, the user is prompted, where the default is the name at
       the cursor, obtained after stripping off any enclosing square
       brackets (@('[..]')), angle brackets (@('<..>')) as from srclink tags, and
       package prefixes.  With @('control-u') prefix argument, search only
       ACL2 source definitions; otherwise, books are searched as well.
       As with built-in Emacs command @('meta-.') , exact matches are given
       priority.  For more information, see the Section on "Selecting a
       Manual" in the acl2-doc online XDOC-based documentation.

    W             acl2-doc-where-definition
       Find an ACL2 definition.  This is the same as
       acl2-doc-definition (the acl2-doc `/' command, as well as
       control-t /), except that the default comes from the name of the
       current page's topic instead of the cursor position.  Searches
       are continued identically when control-t / is given a numeric
       prefix argument, regardless of whether the first command was /,
       control-t /, or W; thus, a search started with W can be continued
       with, for example, meta-3 control-t /.