• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Debugging
    • Projects
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
      • Theories
      • Rule-classes
      • Proof-builder
      • Hons-and-memoization
      • Events
        • Defun
        • Table
        • Memoize
        • Make-event
        • Include-book
        • Encapsulate
        • Defun-sk
        • Defttag
        • Verify-guards
        • Defpkg
        • Mutual-recursion
        • Defattach
        • Defstobj
        • Defchoose
        • Defabsstobj
        • Progn
        • Redundant-events
        • Defmacro
        • In-theory
        • Verify-termination
        • Defconst
        • Embedded-event-form
        • Value-triple
        • Comp
        • Skip-proofs
        • Local
        • Defthm
        • Progn!
        • Defevaluator
        • Assert-event
        • Theory-invariant
        • Defun-inline
        • Define-trusted-clause-processor
        • Partial-encapsulate
        • Defproxy
        • Defexec
        • Defun-nx
        • Defthmg
        • Logical-name
        • Defpun
        • Defabbrev
        • Add-custom-keyword-hint
        • Defrec
        • Regenerate-tau-database
        • Name
        • Deftheory
        • Deftheory-static
        • Defcong
        • Defaxiom
        • Evisc-table
        • Defund
        • Verify-guards+
        • Profile
        • Defequiv
        • Defmacro-untouchable
        • Defthmr
        • Defstub
        • Deflabel
        • Defrefinement
        • In-arithmetic-theory
        • Defabsstobj-missing-events
        • Defthmd
        • Set-body
        • Unmemoize
        • Defun-notinline
        • Dump-events
        • Defund-nx
        • Defun$
        • Remove-custom-keyword-hint
        • Dft
        • Defthy
        • Defund-notinline
        • Defnd
        • Defn
        • Defund-inline
        • Defmacro-last
        • Defdoc
        • History
        • Parallelism
        • Programming
        • Real
        • ACL2-tutorial
        • Debugging
        • Miscellaneous
        • Prover-output
        • Built-in-theorems
        • Macros
        • Interfacing-tools
        • About-ACL2
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • Testing-utilities
      • Math
    • Events

    Defdoc

    Deprecated event (formerly for adding documentation)

    This event is deprecated; see xdoc for information about documentation in ACL2. Defdoc events are never considered redundant (see redundant-events).