These books are not a part of the ACL2 distribution; they were developed for classroom use and are distributed with Dracula. Some of them make use of DrScheme’s imperative capabilities such as interactive animations and automated unit testing.
3.2.1 "audio"
3.2.2 "avl-rational-keys"
3.2.3 "binary-io-utilities"
3.2.4 "doublecheck"
3.2.5 "io-utilities"
3.2.6 "list-utilities"
3.2.7 "rand"
3.2.8 "testing"
3.2.9 "world"