; cd /v/filer4b/v11q001/text/marktoberdorf-08/scripts
; v33

(ld '(

(certify-book "perm")
(u)

(defpkg  "M1"
  (set-difference-equal
   (union-eq '(defp measure l< delta preprocess fast-loop fast correct-loop correct
                pairlis-x2)
         (union-eq *common-lisp-symbols-from-main-lisp-package*
                   *acl2-exports*))
   '(PC PROGRAM ID PUSH POP STEP COMPILE)))

(certify-book "m1" 1)
(u)
(u)

(include-book "m1")
(certify-book "compile" 1)
(u)
(u)

(include-book "m1")
(certify-book "g-direct" 1)
(u)
(u)

(include-book "m1")
(certify-book "g-invariant" 1)
(u)
(u)

(certify-book "utilities")
(u)

(certify-book "fast")
(u)

(include-book "m1")
(certify-book "m1-fast" 1)
(u)

; The preliminary material depends on "fast".
(defpkg  "M1"
  (set-difference-equal
   (union-eq '(defp measure l< delta preprocess fast-loop fast correct-loop correct
                pairlis-x2)
         (union-eq *common-lisp-symbols-from-main-lisp-package*
                   *acl2-exports*))
   '(PC PROGRAM ID PUSH POP STEP COMPILE)))
(certify-book "preliminary-material" 1)
(u)
(u)

)

:ld-pre-eval-print t)