Included Books
hl-addr-combine
extend-pathname
verified-termination-and-guards
sublis-var
subcor-var
subst-expr
subst-var
convert-normalized-term-to-pairs
meta-extract
legal-variablep
merge-sort-term-order
termp
kestrel
remove-guard-holders
merge-sort-symbol-lt
pseudo-good-worldp
bind-macro-args
case-match
fmx-cw
all-fnnames
observation1-cw
defstobj
other
(in-package "ACL2")
include-book
(include-book "hl-addr-combine")
include-book
(include-book "extend-pathname")
include-book
(include-book "verified-termination-and-guards")
include-book
(include-book "sublis-var")
include-book
(include-book "subcor-var")
include-book
(include-book "subst-expr")
include-book
(include-book "subst-var")
include-book
(include-book "convert-normalized-term-to-pairs")
include-book
(include-book "meta-extract")
include-book
(include-book "legal-variablep")
include-book
(include-book "merge-sort-term-order")
include-book
(include-book "termp")
include-book
(include-book "kestrel")
include-book
(include-book "remove-guard-holders")
include-book
(include-book "merge-sort-symbol-lt")
include-book
(include-book "pseudo-good-worldp")
include-book
(include-book "bind-macro-args")
include-book
(include-book "case-match")
include-book
(include-book "fmx-cw")
include-book
(include-book "all-fnnames")
include-book
(include-book "observation1-cw")
include-book
(include-book "defstobj")