Dracula: Reference Manual

This manual defines the ACL2 and Modular ACL2 languages provided by Dracula. For a gentler introduction to Dracula, see Dracula: A Guide to ACL2 in DrScheme. For documentation on the ACL2 theorem prover itself, see the ACL2 home page.

    1 ACL2

    2 Teachpacks

    3 Modular ACL2

    Index