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 Theorem Proving in DrRacket. For documentation on the ACL2 theorem prover itself, see the ACL2 home page.