Included Books
other
(in-package "ACL2")
include-book
(include-book "meta-plus-equal")
include-book
(include-book "meta-plus-lessp")
include-book
(include-book "meta-times-equal")
(in-package "ACL2")
(include-book "meta-plus-equal")
(include-book "meta-plus-lessp")
(include-book "meta-times-equal")