The string ``
ACL'').
When a command is read, all the symbols in it are converted to uppercase.
Thus, typing
(defun app ...) is the same as typing
(DEFUN APP ...) or
(defun App ...). There are ways to force lowercase case characters into
symbols but we won't discuss them here. A consequence of Common Lisp's
default uppercasing is that you'll see a general lack of concern over the
case used when symbols are displayed in this documentation.
In addition, symbols ``belong'' to ``packages'' which give the user a way to
control namespaces. The prompt tells us which package is the default one,
namely
"ACL2". That means when we call
car, for example, we are
invoking the standard definition of that symbol. If the packager were
"JONES" then
car would refer to the definition of that symbol in
that package (which may or may not be different depending on what symbols
were imported into that package. database. is one that display information about the current
logical world or that ``roll back''.