#lang scribble/doc
@(require scribble/manual scribble/eval "evaluator.ss"
          (for-label "../language/dracula.scm"))

@title[#:style 'toc]{Dracula}

Dracula is a DrScheme language level that provides an interface to the ACL2
theorem prover and emulates its executable component.  This section is still
under construction; for a tutorial, sample code, and instructions to install,
upgrade, or remove Dracula, see the
@link["http://www.ccs.neu.edu/home/cce/acl2"]{Dracula webpage}.