Dracula: Reference Manual

This manual defines the ACL2 and Modular ACL2 languages provided by Dracula. For a gentler introduction to Dracula, see (part ("(planet guide.scrbl (cce dracula.plt 8 1) guide)" "top")). For documentation on the ACL2 theorem prover itself, see the ACL2 home page.