|
|
|---|
|
|
|
|---|
Map documentation topics to the community books that define them
The table below maps topics to book locations that reside only in the ACL2+Books combined manual, not the ACL2 User's Manual. For example, the entry
(b* "[books]/std/util/bstar.lisp")
signifies that the topic
((*acl2-system-exports* "[books]/system/acl2-system-exports.lisp") (<< "[books]/misc/total-order.lisp") (add-io-pairs "[books]/std/util/add-io-pairs.lisp") (append-without-guard "[books]/std/lists/flatten.lisp") (oslib::argv "[books]/oslib/argv-logic.lisp") (arith-equivs "[books]/std/basic/arith-equiv-defs.lisp") (arithmetic "[books]/doc/more-topics.lisp") (arithmetic-1 "[books]/arithmetic/top.lisp") (arithmetic/natp-posp "[books]/arithmetic/natp-posp.lisp") (arity+ "[books]/kestrel/std/system/arity-plus.lisp") (assert! "[books]/std/testing/assert-bang.lisp") (assert!-stobj "[books]/std/testing/assert-bang-stobj.lisp") (b* "[books]/std/util/bstar.lisp") (bridge "[books]/centaur/bridge/top.lisp") (oslib::argv "[books]/oslib/catpath.lisp") (build::cert.pl "[books]/build/doc.lisp") (build::cert_param "[books]/build/doc.lisp") (cgen "[books]/acl2s/cgen/top.lisp") (checkpoint-list "[books]/kestrel/utilities/checkpoints-doc.lisp") (consideration "[books]/hints/consider-hint.lisp") (build::custom-certify-book-commands "[books]/build/doc.lisp") (std::defaggregate "[books]/std/util/defaggregate.lisp") (defconsts "[books]/std/util/defconsts.lisp") (defdata "[books]/acl2s/defdata/top.lisp") (define "[books]/std/util/define.lisp") (defmac "[books]/misc/defmac.lisp") (defmacroq "[books]/kestrel/utilities/defmacroq.lisp") (fty::defprod "[books]/centaur/fty/top.lisp") (defpun "[books]/misc/defpun.lisp") (defthm<w "[books]/kestrel/utilities/auto-instance.lisp") (defthmg "[books]/tools/defthmg.lisp") (acl2s::defunc "[books]/acl2s/defunc.lisp") (defxdoc "[books]/xdoc/topics.lisp") (getopt-demo::demo2 "[books]/centaur/getopt/demo2.lisp") (developers-guide "[books]/system/doc/developers-guide.lisp") (developers-guide-utilities "[books]/system/doc/developers-guide.lisp") (do-not-hint "[books]/tools/do-not.lisp") (easy-simplify-term "[books]/tools/easy-simplify.lisp") (er-soft+ "[books]/kestrel/utilities/er-soft-plus.lisp") (er-soft-logic "[books]/tools/er-soft-logic.lisp") (final-cdr "[books]/std/lists/final-cdr.lisp") (fty "[books]/centaur/fty/top.lisp") (getopt "[books]/centaur/getopt/top.lisp") (gl "[books]/centaur/gl/doc.lisp") (hacker "[books]/hacking/hacking-xdoc.lisp") (ihs "[books]/ihs/ihs-doc-topic.lisp") (include-raw "[books]/tools/include-raw.lisp") (install-not-normalized "[books]/misc/install-not-normalized.lisp") (list-equiv "[books]/std/lists/equiv.lisp") (list-fix "[books]/std/lists/list-fix.lisp") (logbitp-reasoning "[books]/centaur/bitops/equal-by-logbitp.lisp") (make-flag "[books]/tools/flag.lisp") (make-termination-theorem "[books]/kestrel/utilities/make-termination-theorem.lisp") (memoized-prover-fns "[books]/tools/memoize-prover-fns.lisp") (must-fail "[books]/std/testing/must-fail.lisp") (str::nat-to-dec-string "[books]/std/strings/decimal.lisp") (non-parallel-book "[books]/std/system/non-parallel-book.lisp") (note-6-4-books "[books]/doc/relnotes.lisp") (note-6-5-books "[books]/doc/relnotes.lisp") (note-7-0-books "[books]/doc/relnotes.lisp") (note-7-1-books "[books]/doc/relnotes.lisp") (note-7-2-books "[books]/doc/relnotes.lisp") (note-8-0-books "[books]/doc/relnotes.lisp") (note-8-1-books "[books]/doc/relnotes.lisp") (note-8-2-books "[books]/doc/relnotes.lisp") (note-8-3-books "[books]/doc/relnotes.lisp") (note-8-4-books "[books]/doc/relnotes.lisp") (note-8-5-books "[books]/doc/relnotes.lisp") (note-8-6-books "[books]/doc/relnotes.lisp") (str::numbers "[books]/std/strings/top.lisp") (open-trace-file! "[books]/tools/open-trace-file-bang.lisp") (oracle-timelimit "[books]/tools/oracle-timelimit.lisp") (oslib "[books]/oslib/top-logic.lisp") (patbind-the "[books]/std/util/bstar.lisp") (build::pre-certify-book-commands "[books]/build/doc.lisp") (xdoc::preprocessor "[books]/xdoc/topics.lisp") (str::pretty "[books]/std/strings/pretty.lisp") (str::pretty-printing "[books]/std/strings/pretty.lisp") (profile-acl2 "[books]/centaur/memoize/old/profile.lisp") (profile-all "[books]/centaur/memoize/old/profile.lisp") (prove$ "[books]/tools/prove-dollar.lisp") (quicklisp "[books]/quicklisp/top.lisp") (release-notes-books "[books]/doc/relnotes.lisp") (removable-runes "[books]/tools/removable-runes.lisp") (remove-hyps "[books]/tools/remove-hyps.lisp") (rewrite$ "[books]/tools/rewrite-dollar.lisp") (rewrite-equiv-hint "[books]/coi/util/rewrite-equiv.lisp") (run-script "[books]/tools/run-script.lisp") (satlink::sat-solver-options "[books]/centaur/satlink/top.lisp") (satlink "[books]/centaur/satlink/top.lisp") (xdoc::save "[books]/xdoc/topics.lisp") (xdoc::save-rendered "[books]/xdoc/topics.lisp") (xdoc::save-rendered-event "[books]/xdoc/topics.lisp") (set-max-mem "[books]/centaur/misc/memory-mgmt-logic.lisp") (spacewalk "[books]/centaur/misc/spacewalk.lisp") (std "[books]/std/top.lisp") (std/io "[books]/std/io/top.lisp") (std/strings "[books]/std/strings/top.lisp") (std/util "[books]/std/util/top.lisp") (std::strict-list-recognizers "[books]/std/util/deflist-base.lisp") (subseq-list "[books]/std/lists/subseq.lisp") (trans-eval-error-triple "[books]/kestrel/utilities/trans-eval-error-triple.lisp") (trans-eval-state "[books]/kestrel/utilities/trans-eval-error-triple.lisp") (unsound-read "[books]/std/io/unsound-read.lisp") (untranslate-patterns "[books]/misc/untranslate-patterns.lisp") (use-trivial-ancestors-check "[books]/tools/trivial-ancestors-check.lisp") (build::using-extended-acl2-images "[books]/build/doc.lisp") (with-raw-mode "[books]/hacking/hacking-xdoc.lisp") (with-redef-allowed "[books]/hacking/hacking-xdoc.lisp") (with-timeout "[books]/acl2s/cgen/with-timeout.lisp") (without-subsumption "[books]/tools/without-subsumption.lisp") (working-with-packages "[books]/doc/practices.lisp") (write-list "[books]/misc/file-io.lisp") (xdoc "[books]/xdoc/topics.lisp"))