ihs-definitions

(in-package "ACL2")

(defxdoc ihs-definitions
  :parents (ihs)
  :short "The @('ihs-definitions') book is a simple interface to the books of
definitions in the @(see ihs) library."
  :long "<p>Including the "ihs-definitions" book includes all of the books of
definitions in the IHS library.  Thus, for :PROGRAM mode specification,
simply</p>

@({
    (include-book "ihs-definitions")
})

<p>at the beginning of a specification book.  If you want to do proofs, then
also include the book "ihs-lemmas", e.g.,</p>

@({
    (local (include-book "ihs-lemmas"))
})

<p>which will include all of ihs lemma books; see @(see ihs-lemmas).</p>")