restrictions on the forms inside books Major Section:  BOOKS
Example Book:  ; This book defines my app function and the
theorem that it is ; associative.  One irrelevant help lemma is
proved first but ; it is local and so not seen by include-book.
I depend on the ; inferior book "weird-list-primitives" from
which I get ; definitions of hd and tl.  (in-package "MY-PKG")
(include-book "weird-list-primitives")  (defun app (x y) (if
(consp x) (cons (hd x) (app (tl x) y)) y))   (defthm help-lemma
(implies (true-listp x) (equal (app x nil) x))))  (defthm app-
is-associative   (equal (app (app a b) c) (app a (app b c))))
The first form in a book must be (in-package "pkg") where "pkg"
is some package name known to ACL2 whenever the book is
certified. The rest of the forms in a book are embedded event
forms, i.e., defuns, defthms, etc., some of which may be marked
local. See embedded-event-form. The usual Common Lisp commenting
conventions are provided. Note that since a book consists of
embedded event forms, we