(IN-PACKAGE "ACL2") "ACL2 Version 3.4" :BEGIN-PORTCULLIS-CMDS :END-PORTCULLIS-CMDS NIL (("/Users/cce/plt/research/dracula/release/src/teachpacks/list-theory.lisp" "list-theory" "list-theory" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 268151760) ("/Users/cce/Local/ACL2/3.4/openmcl64/books/data-structures/list-theory.lisp" "data-structures/list-theory" "list-theory" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 232337215) ("/Users/cce/Local/ACL2/3.4/openmcl64/books/data-structures/deflist.lisp" "deflist" "deflist" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 61371400) (LOCAL ("/Users/cce/Local/ACL2/3.4/openmcl64/books/data-structures/list-defthms.lisp" "list-defthms" "list-defthms" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 209425788)) ("/Users/cce/Local/ACL2/3.4/openmcl64/books/data-structures/utilities.lisp" "utilities" "utilities" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 58465099) ("/Users/cce/Local/ACL2/3.4/openmcl64/books/data-structures/list-defthms.lisp" "list-defthms" "list-defthms" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 209425788) (LOCAL ("/Users/cce/Local/ACL2/3.4/openmcl64/books/arithmetic/equalities.lisp" "arithmetic/equalities" "equalities" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 246711833)) (LOCAL ("/Users/cce/Local/ACL2/3.4/openmcl64/books/cowles/acl2-crg.lisp" "cowles/acl2-crg" "acl2-crg" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 260688904)) (LOCAL ("/Users/cce/Local/ACL2/3.4/openmcl64/books/cowles/acl2-agp.lisp" "acl2-agp" "acl2-agp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 106260818)) (LOCAL ("/Users/cce/Local/ACL2/3.4/openmcl64/books/cowles/acl2-asg.lisp" "acl2-asg" "acl2-asg" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 44566077)) ("/Users/cce/Local/ACL2/3.4/openmcl64/books/data-structures/list-defuns.lisp" "list-defuns" "list-defuns" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 14915098)) 99602905