(in-package "ACL2")

; Change the path if necessary, but then also reflect that change in Makefile.
(include-book "../arithmetic/top-with-meta")