Included Books
apply-fn-into-ifs
apply-term
apply-terms-same-args
apply-unary-to-terms
close-lambdas
conjoin
conjoin-equalities
dumb-negate-lit
fapply-term
fapply-terms-same-args
fapply-unary-to-terms
flatten-ands-in-lit
fsubcor-var
fsublis-fn
fsublis-var
fsublis-var-more-theorems
implicate
make-mv-let-call
make-mv-nth-calls
mvify
quote-term
quote-term-list
remove-dead-if-branches
remove-mbe
remove-progn
remove-trivial-vars
remove-unused-vars
untranslate-dollar
other
(in-package "ACL2")
include-book
(include-book "apply-fn-into-ifs")
include-book
(include-book "apply-term")
include-book
(include-book "apply-terms-same-args")
include-book
(include-book "apply-unary-to-terms")
include-book
(include-book "close-lambdas")
include-book
(include-book "conjoin")
include-book
(include-book "conjoin-equalities")
include-book
(include-book "dumb-negate-lit")
include-book
(include-book "fapply-term")
include-book
(include-book "fapply-terms-same-args")
include-book
(include-book "fapply-unary-to-terms")
include-book
(include-book "flatten-ands-in-lit")
include-book
(include-book "fsubcor-var")
include-book
(include-book "fsublis-fn")
include-book
(include-book "fsublis-var")
include-book
(include-book "fsublis-var-more-theorems")
include-book
(include-book "implicate")
include-book
(include-book "make-mv-let-call")
include-book
(include-book "make-mv-nth-calls")
include-book
(include-book "mvify")
include-book
(include-book "quote-term")
include-book
(include-book "quote-term-list")
include-book
(include-book "remove-dead-if-branches")
include-book
(include-book "remove-mbe")
include-book
(include-book "remove-progn")
include-book
(include-book "remove-trivial-vars")
include-book
(include-book "remove-unused-vars")
include-book
(include-book "untranslate-dollar")
other
(defxdoc std/system/term-transformations :parents (std/system) :short "Utilities to transform terms.")