book-thms

(defun newly-defined-top-level-thms-rec
  (trips collect-p full-book-name acc translated-p)
  (cond ((endp trips) acc)
    ((and (eq (caar trips) 'include-book-path)
       (eq (cadar trips) 'global-value)) (newly-defined-top-level-thms-rec (cdr trips)
        (equal (car (cddar trips)) full-book-name)
        full-book-name
        acc
        translated-p))
    ((not collect-p) (newly-defined-top-level-thms-rec (cdr trips)
        nil
        full-book-name
        acc
        translated-p))
    ((eq (cadar trips)
       (if translated-p
         'theorem
         'untranslated-theorem)) (newly-defined-top-level-thms-rec (cdr trips)
        collect-p
        full-book-name
        (acons (caar trips) (cddar trips) acc)
        translated-p))
    (t (newly-defined-top-level-thms-rec (cdr trips)
        collect-p
        full-book-name
        acc
        translated-p))))

(defun reversed-world-since-event
  (wrld ev acc)
  (cond ((or (endp wrld)
       (let ((trip (car wrld)))
         (and (eq (car trip) 'event-landmark)
           (eq (cadr trip) 'global-value)
           (equal (access-event-tuple-form (cddr trip)) ev)))) acc)
    (t (reversed-world-since-event (cdr wrld)
        ev
        (cons (car wrld) acc)))))

(defun reversed-world-since-boot-strap
  (wrld)
  (reversed-world-since-event wrld
    '(exit-boot-strap-mode)
    nil))

(defun book-thms-fn
  (book-name translated-p state)
  (declare (xargs :stobjs state))
  (mv-let (full-book-string full-book-name
      directory-name
      familiar-name)
    (parse-book-name (cbd) book-name ".lisp" 'book-thms state)
    (declare (ignore full-book-string directory-name familiar-name))
    (newly-defined-top-level-thms-rec (reversed-world-since-boot-strap (w state))
      nil
      full-book-name
      nil
      translated-p)))

(defun theorems-introduced-in
  (book-name state)
  (declare (xargs :stobjs state))
  (strip-cars (book-thms-fn book-name t state)))

(defun new-formula-info1
  (trip wrld acc)
  (let ((name (car trip)) (prop (cddr trip)))
    (case (cadr trip)
      (theorem (cons (list name :theorem prop) acc))
      (unnormalized-body (cond ((eq (car (getprop name
                 'constraint-lst-etc
                 '(t)
                 'current-acl2-world
                 wrld))
             t) (cons (list name
                :def `(equal (,NAME ,@(FORMALS NAME WRLD))
                  ,(UNTRANSLATE PROP NIL WRLD)))
              acc))
          (t acc)))
      (constraint-lst-etc (cond ((and (car prop) (symbolp (car prop))) acc)
          (t (cons (list (getprop name 'siblings nil 'current-acl2-world wrld)
                :constraint (untranslate (cons 'and (car prop)) t wrld))
              acc))))
      (defchoose-axiom (cons (list name :defchoose (untranslate prop t wrld)) acc))
      (global-value (if (and (eq name 'event-landmark)
            (eq (access-event-tuple-type prop) 'table))
          (let ((form (access-event-tuple-form prop)))
            (if (and (eq (first form) 'table)
                (eq (second form) 'acl2-xdoc)
                (eq (third form) :fragment)
                (stringp (fourth form)))
              (cons (fourth form) acc)
              acc))
          acc))
      (t acc))))

(defun new-formula-info
  (trips wrld acc)
  (if (endp trips)
    acc
    (let ((acc (new-formula-info1 (car trips) wrld acc)))
      (new-formula-info (cdr trips) wrld acc))))