Filtering...

loop

books/projects/apply/loop

Included Books

apply loop-lemmas definductor relink-fancy-scion
other
(in-package "ACL2")
other
(deflabel beginning-of-loop-book)
include-book
(include-book "apply")
include-book
(include-book "loop-lemmas")
include-book
(include-book "definductor")
include-book
(include-book "relink-fancy-scion")
other
(make-event (let ((world (w state)))
    `(deftheory loop-book-theory
      ',(SET-DIFFERENCE-EQUAL (CURRENT-THEORY :HERE)
                       (CURRENT-THEORY 'BEGINNING-OF-LOOP-BOOK)))))
other
(make-event (let ((world (w state)))
    `(deftheory loop-rules-theory
      ',(SET-DIFFERENCE-EQUAL (THEORY 'LOOP-BOOK-THEORY) (THEORY 'APPLY-BOOK-THEORY)))))