[Gcl-devel] P.S. on one more Debian/ACL2 issue

[Matt Kaufmann]

P.S. By the way, I'm wondering now if I wouldn't see that error even if I had
installed everything "properly".  So I suggest that you start up ACL2 from a
proposed Debian release (preferably on a machine other than where it was built)
and try

(include-book "/usr/share/acl2-2.7/books/arithmetic/top")

and see if that works.

-- Matt