Search-engine friendly clone of the
ACL2 documentation
.
Top
Documentation
Books
Boolean-reasoning
Projects
Debugging
Std
Proof-automation
Macro-libraries
ACL2
Theories
Rule-classes
Proof-builder
Recursion-and-induction
Hons-and-memoization
Events
Defun
Verify-guards
Table
Mutual-recursion
Memoize
Make-event
Include-book
Encapsulate
Defun-sk
Define-sk
Quantifier-tutorial
Defun-sk-queries
Quantifiers
Defun-sk-example
Defund-sk
Forall
Def::un-sk
Skosimp
Inst?
Equiv
Exists
Congruence
Defttag
Defstobj
Defpkg
Defattach
Defabsstobj
Defchoose
Progn
Verify-termination
Redundant-events
Defmacro
Defconst
Skip-proofs
In-theory
Embedded-event-form
Value-triple
Comp
Local
Defthm
Progn!
Defevaluator
Theory-invariant
Assert-event
Defun-inline
Project-dir-alist
Partial-encapsulate
Define-trusted-clause-processor
Defproxy
Defexec
Defun-nx
Defthmg
Defpun
Defabbrev
Set-table-guard
Name
Defrec
Add-custom-keyword-hint
Regenerate-tau-database
Defcong
Deftheory
Defaxiom
Deftheory-static
Defund
Evisc-table
Verify-guards+
Logical-name
Profile
Defequiv
Defmacro-untouchable
Add-global-stobj
Defthmr
Defstub
Defrefinement
Deflabel
In-arithmetic-theory
Unmemoize
Defabsstobj-missing-events
Defthmd
Fake-event
Set-body
Defun-notinline
Functions-after
Macros-after
Dump-events
Defund-nx
Defun$
Remove-global-stobj
Remove-custom-keyword-hint
Dft
Defthy
Defund-notinline
Defnd
Defn
Defund-inline
Defmacro-last
Parallelism
History
Programming
Operational-semantics
Real
Start-here
Debugging
Miscellaneous
Output-controls
Macros
Interfacing-tools
Interfacing-tools
Hardware-verification
Software-verification
Math
Testing-utilities
Def::un-sk
Inst?
A hint that attempts automated instantiation of quantified formulae
See
def::un-sk
