;; Silly file to trick cert.pl into including the right books.

(in-package "ACL2")

#||
(include-book "ordinals/lexicographic-ordering" :dir :system)
(include-book "data-structures/list-defuns"  :dir :system)
(include-book "data-structures/list-defthms"  :dir :system)
(include-book "make-event/defspec"  :dir :system)
(include-book "data-structures/list-defuns"  :dir :system)
(include-book "data-structures/list-defthms"  :dir :system)
(include-book "meta/term-defuns" :dir :system)
||#