ACL2_PACKAGE_STRUCTURE :=
[
("&", "ACL2-USER", "ACL2"),
("*ACL2-EXPORTS*", "ACL2-USER", "ACL2"),
("*COMMON-LISP-SPECIALS-AND-CONSTANTS*", "ACL2-USER", "ACL2"),
("*COMMON-LISP-SYMBOLS-FROM-MAIN-LISP-PACKAGE*", "ACL2-USER", "ACL2"),
("*MAIN-LISP-PACKAGE-NAME*", "ACL2-USER", "ACL2"),
("*STANDARD-CHARS*", "ACL2-USER", "ACL2"),
("*STANDARD-CI*", "ACL2-USER", "ACL2"),
("*STANDARD-CO*", "ACL2-USER", "ACL2"),
("*STANDARD-OI*", "ACL2-USER", "ACL2"),
("32-BIT-INTEGER-LISTP", "ACL2-USER", "ACL2"),
("32-BIT-INTEGER-LISTP-FORWARD-TO-INTEGER-LISTP", "ACL2-USER", "ACL2"),
("32-BIT-INTEGER-STACK", "ACL2-USER", "ACL2"),
("32-BIT-INTEGER-STACK-LENGTH", "ACL2-USER", "ACL2"),
("32-BIT-INTEGER-STACK-LENGTH1", "ACL2-USER", "ACL2"),
("32-BIT-INTEGERP", "ACL2-USER", "ACL2"),
("32-BIT-INTEGERP-FORWARD-TO-INTEGERP", "ACL2-USER", "ACL2"),
("<-ON-OTHERS", "ACL2-USER", "ACL2"),
("?-FN", "ACL2-USER", "ACL2"),
("@", "ACL2-USER", "ACL2"),
("ABORT!", "ACL2-USER", "ACL2"),
("ACCUMULATED-PERSISTENCE", "ACL2-USER", "ACL2"),
("ACL2-COUNT", "ACL2-USER", "ACL2"),
("ACL2-INPUT-CHANNEL-PACKAGE", "ACL2-USER", "ACL2"),
("ACL2-NUMBERP", "ACL2-USER", "ACL2"),
("ACL2-OUTPUT-CHANNEL-PACKAGE", "ACL2-USER", "ACL2"),
("ACL2-PACKAGE", "ACL2-USER", "ACL2"),
("ADD-DEFAULT-HINTS", "ACL2-USER", "ACL2"),
("ADD-DEFAULT-HINTS!", "ACL2-USER", "ACL2"),
("ADD-INVISIBLE-FNS", "ACL2-USER", "ACL2"),
("ADD-MACRO-ALIAS", "ACL2-USER", "ACL2"),
("ADD-NTH-ALIAS", "ACL2-USER", "ACL2"),
("ADD-PAIR", "ACL2-USER", "ACL2"),
("ADD-PAIR-PRESERVES-ALL-BOUNDP", "ACL2-USER", "ACL2"),
("ADD-TIMERS", "ACL2-USER", "ACL2"),
("ADD-TO-SET-EQ", "ACL2-USER", "ACL2"),
("ADD-TO-SET-EQL", "ACL2-USER", "ACL2"),
("ADD-TO-SET-EQUAL", "ACL2-USER", "ACL2"),
("ALISTP", "ACL2-USER", "ACL2"),
("ALISTP-FORWARD-TO-TRUE-LISTP", "ACL2-USER", "ACL2"),
("ALL-BOUNDP", "ACL2-USER", "ACL2"),
("ALL-BOUNDP-PRESERVES-ASSOC", "ACL2-USER", "ACL2"),
("ALL-VARS", "ACL2-USER", "ACL2"),
("ALL-VARS1", "ACL2-USER", "ACL2"),
("ALL-VARS1-LST", "ACL2-USER", "ACL2"),
("ALPHA-CHAR-P-FORWARD-TO-CHARACTERP", "ACL2-USER", "ACL2"),
("AND-MACRO", "ACL2-USER", "ACL2"),
("AREF-32-BIT-INTEGER-STACK", "ACL2-USER", "ACL2"),
("AREF-T-STACK", "ACL2-USER", "ACL2"),
("AREF1", "ACL2-USER", "ACL2"),
("AREF2", "ACL2-USER", "ACL2"),
("ARGS", "ACL2-USER", "ACL2"),
("ARRAY1P", "ACL2-USER", "ACL2"),
("ARRAY1P-CONS", "ACL2-USER", "ACL2"),
("ARRAY1P-FORWARD", "ACL2-USER", "ACL2"),
("ARRAY1P-LINEAR", "ACL2-USER", "ACL2"),
("ARRAY2P", "ACL2-USER", "ACL2"),
("ARRAY2P-CONS", "ACL2-USER", "ACL2"),
("ARRAY2P-FORWARD", "ACL2-USER", "ACL2"),
("ARRAY2P-LINEAR", "ACL2-USER", "ACL2"),
("ASET-32-BIT-INTEGER-STACK", "ACL2-USER", "ACL2"),
("ASET-T-STACK", "ACL2-USER", "ACL2"),
("ASET1", "ACL2-USER", "ACL2"),
("ASET2", "ACL2-USER", "ACL2"),
("ASSIGN", "ACL2-USER", "ACL2"),
("ASSOC-ADD-PAIR", "ACL2-USER", "ACL2"),
("ASSOC-EQ", "ACL2-USER", "ACL2"),
("ASSOC-EQ-EQUAL", "ACL2-USER", "ACL2"),
("ASSOC-EQ-EQUAL-ALISTP", "ACL2-USER", "ACL2"),
("ASSOC-EQUAL", "ACL2-USER", "ACL2"),
("ASSOC-KEYWORD", "ACL2-USER", "ACL2"),
("ASSOC-STRING-EQUAL", "ACL2-USER", "ACL2"),
("ASSOC2", "ACL2-USER", "ACL2"),
("ASSOCIATIVITY-OF-*", "ACL2-USER", "ACL2"),
("ASSOCIATIVITY-OF-+", "ACL2-USER", "ACL2"),
("ASSUME", "ACL2-USER", "ACL2"),
("ATOM-LISTP", "ACL2-USER", "ACL2"),
("ATOM-LISTP-FORWARD-TO-TRUE-LISTP", "ACL2-USER", "ACL2"),
("BIG-CLOCK-ENTRY", "ACL2-USER", "ACL2"),
("BIG-CLOCK-NEGATIVE-P", "ACL2-USER", "ACL2"),
("BINARY-*", "ACL2-USER", "ACL2"),
("BINARY-+", "ACL2-USER", "ACL2"),
("BINARY-APPEND", "ACL2-USER", "ACL2"),
("BIND-FREE", "ACL2-USER", "ACL2"),
("BINOP-TABLE", "ACL2-USER", "ACL2"),
("ADD-BINOP", "ACL2-USER", "ACL2"),
("REMOVE-BINOP", "ACL2-USER", "ACL2"),
("REMOVE-INVISIBLE-FNS", "ACL2-USER", "ACL2"),
("BOOLEAN-LISTP", "ACL2-USER", "ACL2"),
("BOOLEAN-LISTP-CONS", "ACL2-USER", "ACL2"),
("BOOLEAN-LISTP-FORWARD", "ACL2-USER", "ACL2"),
("BOOLEAN-LISTP-FORWARD-TO-SYMBOL-LISTP", "ACL2-USER", "ACL2"),
("BOOLEANP", "ACL2-USER", "ACL2"),
("BOOLEANP-CHARACTERP", "ACL2-USER", "ACL2"),
("BOOLEANP-COMPOUND-RECOGNIZER", "ACL2-USER", "ACL2"),
("BOUNDED-INTEGER-ALISTP", "ACL2-USER", "ACL2"),
("BOUNDED-INTEGER-ALISTP-FORWARD-TO-EQLABLE-ALISTP", "ACL2-USER", "ACL2"),
("BOUNDED-INTEGER-ALISTP2", "ACL2-USER", "ACL2"),
("BOUNDP-GLOBAL", "ACL2-USER", "ACL2"),
("BOUNDP-GLOBAL1", "ACL2-USER", "ACL2"),
("BRR", "ACL2-USER", "ACL2"),
("BRR@", "ACL2-USER", "ACL2"),
("BUILD-STATE1", "ACL2-USER", "ACL2"),
("CAR-CDR-ELIM", "ACL2-USER", "ACL2"),
("CAR-CONS", "ACL2-USER", "ACL2"),
("CASE-LIST", "ACL2-USER", "ACL2"),
("CASE-LIST-CHECK", "ACL2-USER", "ACL2"),
("CASE-MATCH", "ACL2-USER", "ACL2"),
("CASE-SPLIT", "ACL2-USER", "ACL2"),
("CASE-TEST", "ACL2-USER", "ACL2"),
("CBD", "ACL2-USER", "ACL2"),
("CDR-CONS", "ACL2-USER", "ACL2"),
("CDRN", "ACL2-USER", "ACL2"),
("CERTIFY-BOOK", "ACL2-USER", "ACL2"),
("CERTIFY-BOOK!", "ACL2-USER", "ACL2"),
("CHAR-CODE-CODE-CHAR-IS-IDENTITY", "ACL2-USER", "ACL2"),
("CHAR-CODE-LINEAR", "ACL2-USER", "ACL2"),
("CHARACTER-LISTP", "ACL2-USER", "ACL2"),
("CHARACTER-LISTP-APPEND", "ACL2-USER", "ACL2"),
("CHARACTER-LISTP-COERCE", "ACL2-USER", "ACL2"),
("CHARACTER-LISTP-FORWARD-TO-EQLABLE-LISTP", "ACL2-USER", "ACL2"),
("CHARACTER-LISTP-REMOVE-DUPLICATES-EQL", "ACL2-USER", "ACL2"),
("CHARACTER-LISTP-REVAPPEND", "ACL2-USER", "ACL2"),
("CHARACTER-LISTP-STRING-DOWNCASE-1", "ACL2-USER", "ACL2"),
("CHARACTER-LISTP-STRING-UPCASE1-1", "ACL2-USER", "ACL2"),
("CHARACTERP-CHAR-DOWNCASE", "ACL2-USER", "ACL2"),
("CHARACTERP-CHAR-UPCASE", "ACL2-USER", "ACL2"),
("CHARACTERP-NTH", "ACL2-USER", "ACL2"),
("CHARACTERP-PAGE", "ACL2-USER", "ACL2"),
("CHARACTERP-RUBOUT", "ACL2-USER", "ACL2"),
("CHARACTERP-TAB", "ACL2-USER", "ACL2"),
("CHECK-VARS-NOT-FREE", "ACL2-USER", "ACL2"),
("CHECKPOINT-FORCED-GOALS", "ACL2-USER", "ACL2"),
("CLAUSE", "ACL2-USER", "ACL2"),
("CLOSE-INPUT-CHANNEL", "ACL2-USER", "ACL2"),
("CLOSE-OUTPUT-CHANNEL", "ACL2-USER", "ACL2"),
("CLOSURE", "ACL2-USER", "ACL2"),
("CODE-CHAR-CHAR-CODE-IS-IDENTITY", "ACL2-USER", "ACL2"),
("CODE-CHAR-TYPE", "ACL2-USER", "ACL2"),
("COERCE-INVERSE-1", "ACL2-USER", "ACL2"),
("COERCE-INVERSE-2", "ACL2-USER", "ACL2"),
("COERCE-OBJECT-TO-STATE", "ACL2-USER", "ACL2"),
("COERCE-STATE-TO-OBJECT", "ACL2-USER", "ACL2"),
("COMMUTATIVITY-OF-*", "ACL2-USER", "ACL2"),
("COMMUTATIVITY-OF-+", "ACL2-USER", "ACL2"),
("COMP", "ACL2-USER", "ACL2"),
("COMPLETION-OF-*", "ACL2-USER", "ACL2"),
("COMPLETION-OF-+", "ACL2-USER", "ACL2"),
("COMPLETION-OF-<", "ACL2-USER", "ACL2"),
("COMPLETION-OF-CAR", "ACL2-USER", "ACL2"),
("COMPLETION-OF-CDR", "ACL2-USER", "ACL2"),
("COMPLETION-OF-CHAR-CODE", "ACL2-USER", "ACL2"),
("COMPLETION-OF-CODE-CHAR", "ACL2-USER", "ACL2"),
("COMPLETION-OF-COERCE", "ACL2-USER", "ACL2"),
("COMPLETION-OF-COMPLEX", "ACL2-USER", "ACL2"),
("COMPLETION-OF-DENOMINATOR", "ACL2-USER", "ACL2"),
("COMPLETION-OF-IMAGPART", "ACL2-USER", "ACL2"),
("COMPLETION-OF-INTERN-IN-PACKAGE-OF-SYMBOL", "ACL2-USER", "ACL2"),
("COMPLETION-OF-NUMERATOR", "ACL2-USER", "ACL2"),
("COMPLETION-OF-REALPART", "ACL2-USER", "ACL2"),
("COMPLETION-OF-SYMBOL-NAME", "ACL2-USER", "ACL2"),
("COMPLETION-OF-SYMBOL-PACKAGE-NAME", "ACL2-USER", "ACL2"),
("COMPLETION-OF-UNARY-/", "ACL2-USER", "ACL2"),
("COMPLETION-OF-UNARY-MINUS", "ACL2-USER", "ACL2"),
("COMPLEX-0", "ACL2-USER", "ACL2"),
("COMPLEX-DEFINITION", "ACL2-USER", "ACL2"),
("COMPLEX-EQUAL", "ACL2-USER", "ACL2"),
("COMPLEX-IMPLIES1", "ACL2-USER", "ACL2"),
("COMPLEX-RATIONALP", "ACL2-USER", "ACL2"),
("COMPRESS1", "ACL2-USER", "ACL2"),
("COMPRESS11", "ACL2-USER", "ACL2"),
("COMPRESS2", "ACL2-USER", "ACL2"),
("COMPRESS21", "ACL2-USER", "ACL2"),
("COMPRESS211", "ACL2-USER", "ACL2"),
("COND-CLAUSESP", "ACL2-USER", "ACL2"),
("COND-MACRO", "ACL2-USER", "ACL2"),
("CONS-EQUAL", "ACL2-USER", "ACL2"),
("CONSP-ASSOC", "ACL2-USER", "ACL2"),
("CONSP-ASSOC-EQ", "ACL2-USER", "ACL2"),
("CURRENT-PACKAGE", "ACL2-USER", "ACL2"),
("CURRENT-THEORY", "ACL2-USER", "ACL2"),
("CW-GSTACK", "ACL2-USER", "ACL2"),
("CW", "ACL2-USER", "ACL2"),
("DECREMENT-BIG-CLOCK", "ACL2-USER", "ACL2"),
("DEFABBREV", "ACL2-USER", "ACL2"),
("DEFAULT", "ACL2-USER", "ACL2"),
("DEFAULT-*-1", "ACL2-USER", "ACL2"),
("DEFAULT-*-2", "ACL2-USER", "ACL2"),
("DEFAULT-+-1", "ACL2-USER", "ACL2"),
("DEFAULT-+-2", "ACL2-USER", "ACL2"),
("DEFAULT-<-1", "ACL2-USER", "ACL2"),
("DEFAULT-<-2", "ACL2-USER", "ACL2"),
("DEFAULT-CAR", "ACL2-USER", "ACL2"),
("DEFAULT-CDR", "ACL2-USER", "ACL2"),
("DEFAULT-CHAR-CODE", "ACL2-USER", "ACL2"),
("DEFAULT-COERCE-1", "ACL2-USER", "ACL2"),
("DEFAULT-COERCE-2", "ACL2-USER", "ACL2"),
("DEFAULT-COERCE-3", "ACL2-USER", "ACL2"),
("DEFAULT-COMPILE-FNS", "ACL2-USER", "ACL2"),
("DEFAULT-COMPLEX-1", "ACL2-USER", "ACL2"),
("DEFAULT-COMPLEX-2", "ACL2-USER", "ACL2"),
("DEFAULT-DEFUN-MODE", "ACL2-USER", "ACL2"),
("DEFAULT-DEFUN-MODE-FROM-STATE", "ACL2-USER", "ACL2"),
("DEFAULT-DENOMINATOR", "ACL2-USER", "ACL2"),
("DEFAULT-IMAGPART", "ACL2-USER", "ACL2"),
("DEFAULT-MEASURE-FUNCTION", "ACL2-USER", "ACL2"),
("DEFAULT-NUMERATOR", "ACL2-USER", "ACL2"),
("DEFAULT-REALPART", "ACL2-USER", "ACL2"),
("DEFAULT-SYMBOL-NAME", "ACL2-USER", "ACL2"),
("DEFAULT-SYMBOL-PACKAGE-NAME", "ACL2-USER", "ACL2"),
("DEFAULT-UNARY-/", "ACL2-USER", "ACL2"),
("DEFAULT-UNARY-MINUS", "ACL2-USER", "ACL2"),
("DEFAULT-VERIFY-GUARDS-EAGERNESS", "ACL2-USER", "ACL2"),
("DEFAULT-WELL-FOUNDED-RELATION", "ACL2-USER", "ACL2"),
("DEFAXIOM", "ACL2-USER", "ACL2"),
("DEFCHOOSE", "ACL2-USER", "ACL2"),
("DEFCONG", "ACL2-USER", "ACL2"),
("DEFCONST", "ACL2-USER", "ACL2"),
("DEFDOC", "ACL2-USER", "ACL2"),
("DEFEQUIV", "ACL2-USER", "ACL2"),
("DEFEVALUATOR", "ACL2-USER", "ACL2"),
("DEFEXEC", "ACL2-USER", "ACL2"),
("DEFINE-PC-ATOMIC-MACRO", "ACL2-USER", "ACL2"),
("DEFINE-PC-HELP", "ACL2-USER", "ACL2"),
("DEFINE-PC-MACRO", "ACL2-USER", "ACL2"),
("DEFLABEL", "ACL2-USER", "ACL2"),
("DEFPKG", "ACL2-USER", "ACL2"),
("DEFREFINEMENT", "ACL2-USER", "ACL2"),
("DEFSTOBJ", "ACL2-USER", "ACL2"),
("DEFSTUB", "ACL2-USER", "ACL2"),
("DEFTHEORY", "ACL2-USER", "ACL2"),
("DEFTHM", "ACL2-USER", "ACL2"),
("DEFTHMD", "ACL2-USER", "ACL2"),
("DEFUND", "ACL2-USER", "ACL2"),
("DEFUN-SK", "ACL2-USER", "ACL2"),
("DEFUNS", "ACL2-USER", "ACL2"),
("DELETE-PAIR", "ACL2-USER", "ACL2"),
("DIGIT-TO-CHAR", "ACL2-USER", "ACL2"),
("DIMENSIONS", "ACL2-USER", "ACL2"),
("DISABLE", "ACL2-USER", "ACL2"),
("DISABLE-FORCING", "ACL2-USER", "ACL2"),
("DISABLEDP", "ACL2-USER", "ACL2"),
("DISTRIBUTIVITY", "ACL2-USER", "ACL2"),
("DOC", "ACL2-USER", "ACL2"),
("DOC!", "ACL2-USER", "ACL2"),
("DOCS", "ACL2-USER", "ACL2"),
("DUPLICATES", "ACL2-USER", "ACL2"),
("E/D", "ACL2-USER", "ACL2"),
("E0-ORD-<", "ACL2-USER", "ACL2"),
("E0-ORDINALP", "ACL2-USER", "ACL2"),
("ELIMINATE-DESTRUCTORS", "ACL2-USER", "ACL2"),
("ELIMINATE-IRRELEVANCE", "ACL2-USER", "ACL2"),
("ENABLE", "ACL2-USER", "ACL2"),
("ENABLE-FORCING", "ACL2-USER", "ACL2"),
("ENCAPSULATE", "ACL2-USER", "ACL2"),
("EQLABLE-ALISTP", "ACL2-USER", "ACL2"),
("EQLABLE-ALISTP-FORWARD-TO-ALISTP", "ACL2-USER", "ACL2"),
("EQLABLE-LISTP", "ACL2-USER", "ACL2"),
("EQLABLE-LISTP-FORWARD-TO-ATOM-LISTP", "ACL2-USER", "ACL2"),
("EQLABLEP", "ACL2-USER", "ACL2"),
("EQLABLEP-RECOG", "ACL2-USER", "ACL2"),
("EQUAL-CHAR-CODE", "ACL2-USER", "ACL2"),
("ER", "ACL2-USER", "ACL2"),
("ER-PROGN", "ACL2-USER", "ACL2"),
("ER-PROGN-FN", "ACL2-USER", "ACL2"),
("EVENS", "ACL2-USER", "ACL2"),
("EVENT", "ACL2-USER", "ACL2"),
("EXECUTABLE-COUNTERPART-THEORY", "ACL2-USER", "ACL2"),
("EXPLODE-ATOM", "ACL2-USER", "ACL2"),
("EXPLODE-NONNEGATIVE-INTEGER", "ACL2-USER", "ACL2"),
("EXPT-TYPE-PRESCRIPTION-NON-ZERO-BASE", "ACL2-USER", "ACL2"),
("EXTEND-32-BIT-INTEGER-STACK", "ACL2-USER", "ACL2"),
("EXTEND-T-STACK", "ACL2-USER", "ACL2"),
("EXTEND-WORLD", "ACL2-USER", "ACL2"),
("FERTILIZE", "ACL2-USER", "ACL2"),
("FGETPROP", "ACL2-USER", "ACL2"),
("FILE-CLOCK", "ACL2-USER", "ACL2"),
("FILE-CLOCK-P", "ACL2-USER", "ACL2"),
("FILE-CLOCK-P-FORWARD-TO-INTEGERP", "ACL2-USER", "ACL2"),
("FIRST-N-AC", "ACL2-USER", "ACL2"),
("FIX", "ACL2-USER", "ACL2"),
("FIX-TRUE-LIST", "ACL2-USER", "ACL2"),
("FMS", "ACL2-USER", "ACL2"),
("FMT", "ACL2-USER", "ACL2"),
("FMT-TO-COMMENT-WINDOW", "ACL2-USER", "ACL2"),
("FMT1", "ACL2-USER", "ACL2"),
("FORCE", "ACL2-USER", "ACL2"),
("FUNCTION-SYMBOLP", "ACL2-USER", "ACL2"),
("FUNCTION-THEORY", "ACL2-USER", "ACL2"),
("GENERALIZE", "ACL2-USER", "ACL2"),
("GET-GLOBAL", "ACL2-USER", "ACL2"),
("GET-TIMER", "ACL2-USER", "ACL2"),
("GETPROP-DEFAULT", "ACL2-USER", "ACL2"),
("GETPROPS", "ACL2-USER", "ACL2"),
("GETPROPS1", "ACL2-USER", "ACL2"),
("GLOBAL-TABLE", "ACL2-USER", "ACL2"),
("GLOBAL-TABLE-CARS", "ACL2-USER", "ACL2"),
("GLOBAL-TABLE-CARS1", "ACL2-USER", "ACL2"),
("GLOBAL-VAL", "ACL2-USER", "ACL2"),
("GOOD-BYE", "ACL2-USER", "ACL2"),
("GOOD-DEFUN-MODE-P", "ACL2-USER", "ACL2"),
("GROUND-ZERO", "ACL2-USER", "ACL2"),
("HARD-ERROR", "ACL2-USER", "ACL2"),
("HAS-PROPSP", "ACL2-USER", "ACL2"),
("HAS-PROPSP1", "ACL2-USER", "ACL2"),
("HEADER", "ACL2-USER", "ACL2"),
("HELP", "ACL2-USER", "ACL2"),
("HIDE", "ACL2-USER", "ACL2"),
("I-AM-HERE", "ACL2-USER", "ACL2"),
("ID", "ACL2-USER", "ACL2"),
("IDATES", "ACL2-USER", "ACL2"),
("IF*", "ACL2-USER", "ACL2"),
("IFF", "ACL2-USER", "ACL2"),
("IFF-IMPLIES-EQUAL-IMPLIES-1", "ACL2-USER", "ACL2"),
("IFF-IMPLIES-EQUAL-IMPLIES-2", "ACL2-USER", "ACL2"),
("IFF-IMPLIES-EQUAL-NOT", "ACL2-USER", "ACL2"),
("IFF-IS-AN-EQUIVALENCE", "ACL2-USER", "ACL2"),
("IFIX", "ACL2-USER", "ACL2"),
("ILLEGAL", "ACL2-USER", "ACL2"),
("IMAGPART-COMPLEX", "ACL2-USER", "ACL2"),
("IMMEDIATE-FORCE-MODEP", "ACL2-USER", "ACL2"),
("IMPLIES", "ACL2-USER", "ACL2"),
("IMPROPER-CONSP", "ACL2-USER", "ACL2"),
("IN-THEORY", "ACL2-USER", "ACL2"),
("IN-ARITHMETIC-THEORY", "ACL2-USER", "ACL2"),
("INCLUDE-BOOK", "ACL2-USER", "ACL2"),
("INCOMPATIBLE", "ACL2-USER", "ACL2"),
("INCREMENT-TIMER", "ACL2-USER", "ACL2"),
("INDUCT", "ACL2-USER", "ACL2"),
("INT=", "ACL2-USER", "ACL2"),
("INTEGER-0", "ACL2-USER", "ACL2"),
("INTEGER-1", "ACL2-USER", "ACL2"),
("INTEGER-ABS", "ACL2-USER", "ACL2"),
("INTEGER-IMPLIES-RATIONAL", "ACL2-USER", "ACL2"),
("INTEGER-LISTP", "ACL2-USER", "ACL2"),
("INTEGER-LISTP-FORWARD-TO-RATIONAL-LISTP", "ACL2-USER", "ACL2"),
("INTEGER-STEP", "ACL2-USER", "ACL2"),
("INTERN$", "ACL2-USER", "ACL2"),
("INTERN-IN-PACKAGE-OF-SYMBOL", "ACL2-USER", "ACL2"),
("INTERN-IN-PACKAGE-OF-SYMBOL-SYMBOL-NAME", "ACL2-USER", "ACL2"),
("INTERSECTION-EQ", "ACL2-USER", "ACL2"),
("INTERSECTION-THEORIES", "ACL2-USER", "ACL2"),
("INTERSECTP-EQ", "ACL2-USER", "ACL2"),
("INTERSECTP-EQUAL", "ACL2-USER", "ACL2"),
("INVERSE-OF-*", "ACL2-USER", "ACL2"),
("INVERSE-OF-+", "ACL2-USER", "ACL2"),
("INVISIBLE-FNS-TABLE", "ACL2-USER", "ACL2"),
("KEYWORD-PACKAGE", "ACL2-USER", "ACL2"),
("KEYWORD-VALUE-LISTP", "ACL2-USER", "ACL2"),
("KEYWORD-VALUE-LISTP-ASSOC-KEYWORD", "ACL2-USER", "ACL2"),
("KEYWORD-VALUE-LISTP-FORWARD-TO-TRUE-LISTP", "ACL2-USER", "ACL2"),
("KEYWORDP-FORWARD-TO-SYMBOLP", "ACL2-USER", "ACL2"),
("KNOWN-PACKAGE-ALIST", "ACL2-USER", "ACL2"),
("KNOWN-PACKAGE-ALISTP", "ACL2-USER", "ACL2"),
("KNOWN-PACKAGE-ALISTP-FORWARD-TO-TRUE-LIST-LISTP-AND-ALISTP", "ACL2-USER",
"ACL2"),
("LD", "ACL2-USER", "ACL2"),
("LD-ERROR-ACTION", "ACL2-USER", "ACL2"),
("LD-ERROR-TRIPLES", "ACL2-USER", "ACL2"),
("LD-KEYWORD-ALIASES", "ACL2-USER", "ACL2"),
("LD-POST-EVAL-PRINT", "ACL2-USER", "ACL2"),
("LD-PRE-EVAL-FILTER", "ACL2-USER", "ACL2"),
("LD-PRE-EVAL-PRINT", "ACL2-USER", "ACL2"),
("LD-PROMPT", "ACL2-USER", "ACL2"),
("LD-QUERY-CONTROL-ALIST", "ACL2-USER", "ACL2"),
("LD-REDEFINITION-ACTION", "ACL2-USER", "ACL2"),
("LD-SKIP-PROOFSP", "ACL2-USER", "ACL2"),
("LD-VERBOSE", "ACL2-USER", "ACL2"),
("LEGAL-CASE-CLAUSESP", "ACL2-USER", "ACL2"),
("LEN", "ACL2-USER", "ACL2"),
("LEN-UPDATE-NTH", "ACL2-USER", "ACL2"),
("LIST*-MACRO", "ACL2-USER", "ACL2"),
("LIST-ALL-PACKAGE-NAMES", "ACL2-USER", "ACL2"),
("LIST-ALL-PACKAGE-NAMES-LST", "ACL2-USER", "ACL2"),
("LIST-MACRO", "ACL2-USER", "ACL2"),
("LOCAL", "ACL2-USER", "ACL2"),
("LOGIC", "ACL2-USER", "ACL2"),
("LOWER-CASE-P-CHAR-DOWNCASE", "ACL2-USER", "ACL2"),
("LOWER-CASE-P-FORWARD-TO-ALPHA-CHAR-P", "ACL2-USER", "ACL2"),
("LOWEST-TERMS", "ACL2-USER", "ACL2"),
("LP", "ACL2-USER", "ACL2"),
("MACRO-ALIASES", "ACL2-USER", "ACL2"),
("NTH-ALIASES", "ACL2-USER", "ACL2"),
("MAIN-TIMER", "ACL2-USER", "ACL2"),
("MAIN-TIMER-TYPE-PRESCRIPTION", "ACL2-USER", "ACL2"),
("MAKE-CHARACTER-LIST", "ACL2-USER", "ACL2"),
("MAKE-CHARACTER-LIST-MAKE-CHARACTER-LIST", "ACL2-USER", "ACL2"),
("MAKE-FMT-BINDINGS", "ACL2-USER", "ACL2"),
("MAKE-INPUT-CHANNEL", "ACL2-USER", "ACL2"),
("MAKE-LIST-AC", "ACL2-USER", "ACL2"),
("MAKE-MV-NTHS", "ACL2-USER", "ACL2"),
("MAKE-ORD", "ACL2-USER", "ACL2"),
("MAKE-OUTPUT-CHANNEL", "ACL2-USER", "ACL2"),
("MAKE-VAR-LST", "ACL2-USER", "ACL2"),
("MAKE-VAR-LST1", "ACL2-USER", "ACL2"),
("MAKUNBOUND-GLOBAL", "ACL2-USER", "ACL2"),
("MAXIMUM-LENGTH", "ACL2-USER", "ACL2"),
("MAY-NEED-SLASHES", "ACL2-USER", "ACL2"),
("MBE", "ACL2-USER", "ACL2"),
("MBT", "ACL2-USER", "ACL2"),
("MEMBER-EQ", "ACL2-USER", "ACL2"),
("MEMBER-EQUAL", "ACL2-USER", "ACL2"),
("MEMBER-SYMBOL-NAME", "ACL2-USER", "ACL2"),
("MFC", "ACL2-USER", "ACL2"),
("MINIMAL-THEORY", "ACL2-USER", "ACL2"),
("MONITOR", "ACL2-USER", "ACL2"),
("MONITORED-RUNES", "ACL2-USER", "ACL2"),
("MORE", "ACL2-USER", "ACL2"),
("MORE!", "ACL2-USER", "ACL2"),
("MORE-DOC", "ACL2-USER", "ACL2"),
("MUTUAL-RECURSION", "ACL2-USER", "ACL2"),
("MUTUAL-RECURSION-GUARDP", "ACL2-USER", "ACL2"),
("MV", "ACL2-USER", "ACL2"),
("MV-LET", "ACL2-USER", "ACL2"),
("MV-NTH", "ACL2-USER", "ACL2"),
("NATP", "ACL2-USER", "ACL2"),
("NEWLINE", "ACL2-USER", "ACL2"),
("NFIX", "ACL2-USER", "ACL2"),
("NIL-IS-NOT-CIRCULAR", "ACL2-USER", "ACL2"),
("NO-DUPLICATESP", "ACL2-USER", "ACL2"),
("NO-DUPLICATESP-EQUAL", "ACL2-USER", "ACL2"),
("NONNEGATIVE-INTEGER-QUOTIENT", "ACL2-USER", "ACL2"),
("NONNEGATIVE-PRODUCT", "ACL2-USER", "ACL2"),
("NONZERO-IMAGPART", "ACL2-USER", "ACL2"),
("NQTHM-TO-ACL2", "ACL2-USER", "ACL2"),
("NTH-0-CONS", "ACL2-USER", "ACL2"),
("NTH-0-READ-RUN-TIME-TYPE-PRESCRIPTION", "ACL2-USER", "ACL2"),
("NTH-ADD1", "ACL2-USER", "ACL2"),
("NTH-UPDATE-NTH", "ACL2-USER", "ACL2"),
("O<", "ACL2-USER", "ACL2"),
("O<=", "ACL2-USER", "ACL2"),
("O>", "ACL2-USER", "ACL2"),
("O>=", "ACL2-USER", "ACL2"),
("O-FINP", "ACL2-USER", "ACL2"),
("O-FIRST-COEFF", "ACL2-USER", "ACL2"),
("O-FIRST-EXPT", "ACL2-USER", "ACL2"),
("O-INFP", "ACL2-USER", "ACL2"),
("O-P", "ACL2-USER", "ACL2"),
("O-RST", "ACL2-USER", "ACL2"),
("OBSERVATION", "ACL2-USER", "ACL2"),
("ODDS", "ACL2-USER", "ACL2"),
("OK-IF", "ACL2-USER", "ACL2"),
("OOPS", "ACL2-USER", "ACL2"),
("OPEN-CHANNEL-LISTP", "ACL2-USER", "ACL2"),
("OPEN-CHANNEL1", "ACL2-USER", "ACL2"),
("OPEN-CHANNEL1-FORWARD-TO-TRUE-LISTP-AND-CONSP", "ACL2-USER", "ACL2"),
("OPEN-CHANNELS-P", "ACL2-USER", "ACL2"),
("OPEN-CHANNELS-P-FORWARD", "ACL2-USER", "ACL2"),
("OPEN-INPUT-CHANNEL", "ACL2-USER", "ACL2"),
("OPEN-INPUT-CHANNEL-ANY-P", "ACL2-USER", "ACL2"),
("OPEN-INPUT-CHANNEL-ANY-P1", "ACL2-USER", "ACL2"),
("OPEN-INPUT-CHANNEL-P", "ACL2-USER", "ACL2"),
("OPEN-INPUT-CHANNEL-P1", "ACL2-USER", "ACL2"),
("OPEN-INPUT-CHANNELS", "ACL2-USER", "ACL2"),
("OPEN-OUTPUT-CHANNEL", "ACL2-USER", "ACL2"),
("OPEN-OUTPUT-CHANNEL-ANY-P", "ACL2-USER", "ACL2"),
("OPEN-OUTPUT-CHANNEL-ANY-P1", "ACL2-USER", "ACL2"),
("OPEN-OUTPUT-CHANNEL-P", "ACL2-USER", "ACL2"),
("OPEN-OUTPUT-CHANNEL-P1", "ACL2-USER", "ACL2"),
("OPEN-OUTPUT-CHANNELS", "ACL2-USER", "ACL2"),
("OR-MACRO", "ACL2-USER", "ACL2"),
("ORDERED-SYMBOL-ALISTP", "ACL2-USER", "ACL2"),
("ORDERED-SYMBOL-ALISTP-ADD-PAIR", "ACL2-USER", "ACL2"),
("ORDERED-SYMBOL-ALISTP-ADD-PAIR-FORWARD", "ACL2-USER", "ACL2"),
("ORDERED-SYMBOL-ALISTP-FORWARD-TO-SYMBOL-ALISTP", "ACL2-USER", "ACL2"),
("ORDERED-SYMBOL-ALISTP-GETPROPS", "ACL2-USER", "ACL2"),
("ORDERED-SYMBOL-ALISTP-REMOVE-FIRST-PAIR", "ACL2-USER", "ACL2"),
("OUR-DIGIT-CHAR-P", "ACL2-USER", "ACL2"),
("PAIRLIS$", "ACL2-USER", "ACL2"),
("PAIRLIS2", "ACL2-USER", "ACL2"),
("PBT", "ACL2-USER", "ACL2"),
("PC", "ACL2-USER", "ACL2"),
("PCB", "ACL2-USER", "ACL2"),
("PCB!", "ACL2-USER", "ACL2"),
("PCS", "ACL2-USER", "ACL2"),
("PE", "ACL2-USER", "ACL2"),
("PE!", "ACL2-USER", "ACL2"),
("PEEK-CHAR$", "ACL2-USER", "ACL2"),
("PF", "ACL2-USER", "ACL2"),
("PL", "ACL2-USER", "ACL2"),
("POP-TIMER", "ACL2-USER", "ACL2"),
("POSITION-AC", "ACL2-USER", "ACL2"),
("POSITION-EQ", "ACL2-USER", "ACL2"),
("POSITION-EQ-AC", "ACL2-USER", "ACL2"),
("POSITION-EQUAL", "ACL2-USER", "ACL2"),
("POSITION-EQUAL-AC", "ACL2-USER", "ACL2"),
("POSITIVE", "ACL2-USER", "ACL2"),
("POSP", "ACL2-USER", "ACL2"),
("POWER-EVAL", "ACL2-USER", "ACL2"),
("PPROGN", "ACL2-USER", "ACL2"),
("PR", "ACL2-USER", "ACL2"),
("PR!", "ACL2-USER", "ACL2"),
("PREPROCESS", "ACL2-USER", "ACL2"),
("PRIN1$", "ACL2-USER", "ACL2"),
("PRIN1-WITH-SLASHES", "ACL2-USER", "ACL2"),
("PRIN1-WITH-SLASHES1", "ACL2-USER", "ACL2"),
("PRINC$", "ACL2-USER", "ACL2"),
("PRINT-OBJECT$", "ACL2-USER", "ACL2"),
("PRINT-RATIONAL-AS-DECIMAL", "ACL2-USER", "ACL2"),
("PRINT-TIMER", "ACL2-USER", "ACL2"),
("PROG2$", "ACL2-USER", "ACL2"),
("PROGRAM", "ACL2-USER", "ACL2"),
("PROOF-TREE", "ACL2-USER", "ACL2"),
("PROOFS-CO", "ACL2-USER", "ACL2"),
("PROPER-CONSP", "ACL2-USER", "ACL2"),
("PROPS", "ACL2-USER", "ACL2"),
("PROVE", "ACL2-USER", "ACL2"),
("PSEUDO-TERM-LISTP", "ACL2-USER", "ACL2"),
("PSEUDO-TERM-LISTP-FORWARD-TO-TRUE-LISTP", "ACL2-USER", "ACL2"),
("PSEUDO-TERMP", "ACL2-USER", "ACL2"),
("PSTACK", "ACL2-USER", "ACL2"),
("PUFF", "ACL2-USER", "ACL2"),
("PUFF*", "ACL2-USER", "ACL2"),
("PUSH-TIMER", "ACL2-USER", "ACL2"),
("PUSH-UNTOUCHABLE", "ACL2-USER", "ACL2"),
("PUT-ASSOC-EQ", "ACL2-USER", "ACL2"),
("PUT-ASSOC-EQUAL", "ACL2-USER", "ACL2"),
("PUT-GLOBAL", "ACL2-USER", "ACL2"),
("PUTPROP", "ACL2-USER", "ACL2"),
("QUOTEP", "ACL2-USER", "ACL2"),
("R-EQLABLE-ALISTP", "ACL2-USER", "ACL2"),
("RASSOC-EQ", "ACL2-USER", "ACL2"),
("RASSOC-EQUAL", "ACL2-USER", "ACL2"),
("RATIONAL-IMPLIES1", "ACL2-USER", "ACL2"),
("RATIONAL-IMPLIES2", "ACL2-USER", "ACL2"),
("RATIONAL-LISTP", "ACL2-USER", "ACL2"),
("RATIONAL-LISTP-FORWARD-TO-TRUE-LISTP", "ACL2-USER", "ACL2"),
("RATIONALP-*", "ACL2-USER", "ACL2"),
("RATIONALP-+", "ACL2-USER", "ACL2"),
("RATIONALP-EXPT-TYPE-PRESCRIPTION", "ACL2-USER", "ACL2"),
("RATIONALP-IMPLIES-ACL2-NUMBERP", "ACL2-USER", "ACL2"),
("RATIONALP-UNARY--", "ACL2-USER", "ACL2"),
("RATIONALP-UNARY-/", "ACL2-USER", "ACL2"),
("READ-BYTE$", "ACL2-USER", "ACL2"),
("READ-CHAR$", "ACL2-USER", "ACL2"),
("READ-FILE-LISTP", "ACL2-USER", "ACL2"),
("READ-FILE-LISTP-FORWARD-TO-TRUE-LIST-LISTP", "ACL2-USER", "ACL2"),
("READ-FILE-LISTP1", "ACL2-USER", "ACL2"),
("READ-FILE-LISTP1-FORWARD-TO-TRUE-LISTP-AND-CONSP", "ACL2-USER", "ACL2"),
("READ-FILES", "ACL2-USER", "ACL2"),
("READ-FILES-P", "ACL2-USER", "ACL2"),
("READ-FILES-P-FORWARD-TO-READ-FILE-LISTP", "ACL2-USER", "ACL2"),
("READ-IDATE", "ACL2-USER", "ACL2"),
("READ-OBJECT", "ACL2-USER", "ACL2"),
("READ-RUN-TIME", "ACL2-USER", "ACL2"),
("READ-RUN-TIME-PRESERVES-STATE-P1", "ACL2-USER", "ACL2"),
("READABLE-FILE", "ACL2-USER", "ACL2"),
("READABLE-FILE-FORWARD-TO-TRUE-LISTP-AND-CONSP", "ACL2-USER", "ACL2"),
("READABLE-FILES", "ACL2-USER", "ACL2"),
("READABLE-FILES-LISTP", "ACL2-USER", "ACL2"),
("READABLE-FILES-LISTP-FORWARD-TO-TRUE-LIST-LISTP-AND-ALISTP", "ACL2-USER",
"ACL2"),
("READABLE-FILES-P", "ACL2-USER", "ACL2"),
("READABLE-FILES-P-FORWARD-TO-READABLE-FILES-LISTP", "ACL2-USER", "ACL2"),
("REAL/RATIONALP", "ACL2-USER", "ACL2"),
("REALFIX", "ACL2-USER", "ACL2"),
("REALPART-COMPLEX", "ACL2-USER", "ACL2"),
("REALPART-IMAGPART-ELIM", "ACL2-USER", "ACL2"),
("REBUILD", "ACL2-USER", "ACL2"),
("REDEF", "ACL2-USER", "ACL2"),
("REDEF!", "ACL2-USER", "ACL2"),
("REMOVE-DEFAULT-HINTS", "ACL2-USER", "ACL2"),
("REMOVE-DEFAULT-HINTS!", "ACL2-USER", "ACL2"),
("REMOVE-DUPLICATES-EQL", "ACL2-USER", "ACL2"),
("REMOVE-DUPLICATES-EQUAL", "ACL2-USER", "ACL2"),
("REMOVE-FIRST-PAIR", "ACL2-USER", "ACL2"),
("REMOVE-MACRO-ALIAS", "ACL2-USER", "ACL2"),
("REMOVE-NTH-ALIAS", "ACL2-USER", "ACL2"),
("RESET-LD-SPECIALS", "ACL2-USER", "ACL2"),
("RETRACT-WORLD", "ACL2-USER", "ACL2"),
("RETRIEVE", "ACL2-USER", "ACL2"),
("RFIX", "ACL2-USER", "ACL2"),
("RUN-TIMES", "ACL2-USER", "ACL2"),
("SET-BOGUS-MUTUAL-RECURSION-OK", "ACL2-USER", "ACL2"),
("SET-CBD", "ACL2-USER", "ACL2"),
("SET-CASE-SPLIT-LIMITATIONS", "ACL2-USER", "ACL2"),
("SET-COMPILE-FNS", "ACL2-USER", "ACL2"),
("SET-DEFAULT-HINTS", "ACL2-USER", "ACL2"),
("SET-DEFAULT-HINTS!", "ACL2-USER", "ACL2"),
("SET-DIFFERENCE-EQ", "ACL2-USER", "ACL2"),
("SET-DIFFERENCE-EQUAL", "ACL2-USER", "ACL2"),
("SET-DIFFERENCE-THEORIES", "ACL2-USER", "ACL2"),
("SET-ENFORCE-REDUNDANCY", "ACL2-USER", "ACL2"),
("SET-EQUALP-EQUAL", "ACL2-USER", "ACL2"),
("SET-GUARD-CHECKING", "ACL2-USER", "ACL2"),
("SET-IGNORE-OK", "ACL2-USER", "ACL2"),
("SET-INHIBIT-OUTPUT-LST", "ACL2-USER", "ACL2"),
("SET-INHIBIT-WARNINGS", "ACL2-USER", "ACL2"),
("SET-INVISIBLE-FNS-TABLE", "ACL2-USER", "ACL2"),
("SET-IRRELEVANT-FORMALS-OK", "ACL2-USER", "ACL2"),
("SET-MEASURE-FUNCTION", "ACL2-USER", "ACL2"),
("SET-NON-LINEARP", "ACL2-USER", "ACL2"),
("SET-STATE-OK", "ACL2-USER", "ACL2"),
("SET-TIMER", "ACL2-USER", "ACL2"),
("SET-VERIFY-GUARDS-EAGERNESS", "ACL2-USER", "ACL2"),
("SET-W", "ACL2-USER", "ACL2"),
("SET-WELL-FOUNDED-RELATION", "ACL2-USER", "ACL2"),
("SGETPROP", "ACL2-USER", "ACL2"),
("SHOW-BDD", "ACL2-USER", "ACL2"),
("SHOW-ACCUMULATED-PERSISTENCE", "ACL2-USER", "ACL2"),
("SHRINK-32-BIT-INTEGER-STACK", "ACL2-USER", "ACL2"),
("SHRINK-T-STACK", "ACL2-USER", "ACL2"),
("SIMPLIFY", "ACL2-USER", "ACL2"),
("SKIP-PROOFS", "ACL2-USER", "ACL2"),
("SOME-SLASHABLE", "ACL2-USER", "ACL2"),
("STABLE-UNDER-SIMPLIFICATIONP", "ACL2-USER", "ACL2"),
("STANDARD-CHAR-LISTP", "ACL2-USER", "ACL2"),
("STANDARD-CHAR-LISTP-APPEND", "ACL2-USER", "ACL2"),
("STANDARD-CHAR-LISTP-FORWARD-TO-CHARACTER-LISTP", "ACL2-USER", "ACL2"),
("STANDARD-CHAR-P-NTH", "ACL2-USER", "ACL2"),
("STANDARD-CO", "ACL2-USER", "ACL2"),
("STANDARD-OI", "ACL2-USER", "ACL2"),
("START-PROOF-TREE", "ACL2-USER", "ACL2"),
("STATE", "ACL2-USER", "ACL2"),
("STATE-GLOBAL-LET*-CLEANUP", "ACL2-USER", "ACL2"),
("STATE-GLOBAL-LET*-GET-GLOBALS", "ACL2-USER", "ACL2"),
("STATE-GLOBAL-LET*-PUT-GLOBALS", "ACL2-USER", "ACL2"),
("STATE-P", "ACL2-USER", "ACL2"),
("STATE-P-IMPLIES-AND-FORWARD-TO-STATE-P1", "ACL2-USER", "ACL2"),
("STATE-P1", "ACL2-USER", "ACL2"),
("STATE-P1-FORWARD", "ACL2-USER", "ACL2"),
("STATE-P1-UPDATE-MAIN-TIMER", "ACL2-USER", "ACL2"),
("STATE-P1-UPDATE-NTH-2-WORLD", "ACL2-USER", "ACL2"),
("STOP-PROOF-TREE", "ACL2-USER", "ACL2"),
("STANDARD-STRING-ALISTP", "ACL2-USER", "ACL2"),
("STANDARD-STRING-ALISTP-FORWARD-TO-ALISTP", "ACL2-USER", "ACL2"),
("STRING-APPEND", "ACL2-USER", "ACL2"),
("STRING-APPEND-LST", "ACL2-USER", "ACL2"),
("STRING-DOWNCASE1", "ACL2-USER", "ACL2"),
("STRING-EQUAL1", "ACL2-USER", "ACL2"),
("STRING-IS-NOT-CIRCULAR", "ACL2-USER", "ACL2"),
("STRING-LISTP", "ACL2-USER", "ACL2"),
("STRING-UPCASE1", "ACL2-USER", "ACL2"),
("STRING<-IRREFLEXIVE", "ACL2-USER", "ACL2"),
("STRING<-L", "ACL2-USER", "ACL2"),
("STRING<-L-ASYMMETRIC", "ACL2-USER", "ACL2"),
("STRING<-L-IRREFLEXIVE", "ACL2-USER", "ACL2"),
("STRING<-L-TRANSITIVE", "ACL2-USER", "ACL2"),
("STRING<-L-TRICHOTOMY", "ACL2-USER", "ACL2"),
("STRINGP-SYMBOL-PACKAGE-NAME", "ACL2-USER", "ACL2"),
("STRIP-CARS", "ACL2-USER", "ACL2"),
("STRIP-CDRS", "ACL2-USER", "ACL2"),
("SUBSEQ-LIST", "ACL2-USER", "ACL2"),
("SUBSETP-EQUAL", "ACL2-USER", "ACL2"),
("SUBSTITUTE-AC", "ACL2-USER", "ACL2"),
("SUMMARY", "ACL2-USER", "ACL2"),
("SYMBOL-<", "ACL2-USER", "ACL2"),
("SYMBOL-<-ASYMMETRIC", "ACL2-USER", "ACL2"),
("SYMBOL-<-IRREFLEXIVE", "ACL2-USER", "ACL2"),
("SYMBOL-<-TRANSITIVE", "ACL2-USER", "ACL2"),
("SYMBOL-<-TRICHOTOMY", "ACL2-USER", "ACL2"),
("SYMBOL-ALISTP", "ACL2-USER", "ACL2"),
("SYMBOL-ALISTP-FORWARD-TO-EQLABLE-ALISTP", "ACL2-USER", "ACL2"),
("SYMBOL-DOUBLET-LISTP", "ACL2-USER", "ACL2"),
("SYMBOL-EQUALITY", "ACL2-USER", "ACL2"),
("SYMBOL-LISTP", "ACL2-USER", "ACL2"),
("SYMBOL-LISTP-FORWARD-TO-TRUE-LISTP", "ACL2-USER", "ACL2"),
("SYMBOL-NAME-INTERN-IN-PACKAGE-OF-SYMBOL", "ACL2-USER", "ACL2"),
("SYMBOL-PACKAGE-NAME", "ACL2-USER", "ACL2"),
("SYMBOLP-INTERN-IN-PACKAGE-OF-SYMBOL", "ACL2-USER", "ACL2"),
("SYNP", "ACL2-USER", "ACL2"),
("SYNTAXP", "ACL2-USER", "ACL2"),
("SYS-CALL", "ACL2-USER", "ACL2"),
("SYS-CALL-STATUS", "ACL2-USER", "ACL2"),
("T-STACK", "ACL2-USER", "ACL2"),
("T-STACK-LENGTH", "ACL2-USER", "ACL2"),
("T-STACK-LENGTH1", "ACL2-USER", "ACL2"),
("TABLE", "ACL2-USER", "ACL2"),
("TABLE-ALIST", "ACL2-USER", "ACL2"),
("TAKE", "ACL2-USER", "ACL2"),
("THE-ERROR", "ACL2-USER", "ACL2"),
("THE-FIXNUM", "ACL2-USER", "ACL2"),
("THE-FIXNUM!", "ACL2-USER", "ACL2"),
("THEORY", "ACL2-USER", "ACL2"),
("THEORY-INVARIANT", "ACL2-USER", "ACL2"),
("THM", "ACL2-USER", "ACL2"),
("TIMER-ALISTP", "ACL2-USER", "ACL2"),
("TIMER-ALISTP-FORWARD-TO-TRUE-LIST-LISTP-AND-SYMBOL-ALISTP", "ACL2-USER",
"ACL2"),
("TOGGLE-PC-MACRO", "ACL2-USER", "ACL2"),
("TRACE$", "ACL2-USER", "ACL2"),
("TRANS", "ACL2-USER", "ACL2"),
("TRANS1", "ACL2-USER", "ACL2"),
("TRICHOTOMY", "ACL2-USER", "ACL2"),
("TRUE-LISTP", "ACL2-USER", "ACL2"),
("TRUE-LIST-LISTP", "ACL2-USER", "ACL2"),
("TRUE-LIST-LISTP-FORWARD-TO-TRUE-LISTP", "ACL2-USER", "ACL2"),
("TRUE-LIST-LISTP-FORWARD-TO-TRUE-LISTP-ASSOC-EQ", "ACL2-USER", "ACL2"),
("TRUE-LISTP-CADR-ASSOC-EQ-FOR-OPEN-CHANNELS-P", "ACL2-USER", "ACL2"),
("TRUE-LISTP-UPDATE-NTH", "ACL2-USER", "ACL2"),
("TYPED-IO-LISTP", "ACL2-USER", "ACL2"),
("TYPED-IO-LISTP-FORWARD-TO-TRUE-LISTP", "ACL2-USER", "ACL2"),
("U", "ACL2-USER", "ACL2"),
("UBT", "ACL2-USER", "ACL2"),
("UBT!", "ACL2-USER", "ACL2"),
("UNARY--", "ACL2-USER", "ACL2"),
("UNARY-/", "ACL2-USER", "ACL2"),
("UNARY-FUNCTION-SYMBOL-LISTP", "ACL2-USER", "ACL2"),
("UNICITY-OF-0", "ACL2-USER", "ACL2"),
("UNICITY-OF-1", "ACL2-USER", "ACL2"),
("UNION-EQ", "ACL2-USER", "ACL2"),
("UNION-EQUAL", "ACL2-USER", "ACL2"),
("UNION-THEORIES", "ACL2-USER", "ACL2"),
("UNIVERSAL-THEORY", "ACL2-USER", "ACL2"),
("UNMONITOR", "ACL2-USER", "ACL2"),
("UNSAVE", "ACL2-USER", "ACL2"),
("UNTRACE$", "ACL2-USER", "ACL2"),
("UPDATE-32-BIT-INTEGER-STACK", "ACL2-USER", "ACL2"),
("UPDATE-BIG-CLOCK-ENTRY", "ACL2-USER", "ACL2"),
("UPDATE-FILE-CLOCK", "ACL2-USER", "ACL2"),
("UPDATE-GLOBAL-TABLE", "ACL2-USER", "ACL2"),
("UPDATE-IDATES", "ACL2-USER", "ACL2"),
("UPDATE-LIST-ALL-PACKAGE-NAMES-LST", "ACL2-USER", "ACL2"),
("UPDATE-NTH", "ACL2-USER", "ACL2"),
("UPDATE-OPEN-INPUT-CHANNELS", "ACL2-USER", "ACL2"),
("UPDATE-OPEN-OUTPUT-CHANNELS", "ACL2-USER", "ACL2"),
("UPDATE-READ-FILES", "ACL2-USER", "ACL2"),
("UPDATE-RUN-TIMES", "ACL2-USER", "ACL2"),
("UPDATE-RUN-TIMES-PRESERVES-STATE-P1", "ACL2-USER", "ACL2"),
("UPDATE-T-STACK", "ACL2-USER", "ACL2"),
("UPDATE-USER-STOBJ-ALIST", "ACL2-USER", "ACL2"),
("UPDATE-USER-STOBJ-ALIST1", "ACL2-USER", "ACL2"),
("UPDATE-WRITTEN-FILES", "ACL2-USER", "ACL2"),
("UPPER-CASE-P-CHAR-UPCASE", "ACL2-USER", "ACL2"),
("UPPER-CASE-P-FORWARD-TO-ALPHA-CHAR-P", "ACL2-USER", "ACL2"),
("USER-STOBJ-ALIST", "ACL2-USER", "ACL2"),
("USER-STOBJ-ALIST1", "ACL2-USER", "ACL2"),
("VERBOSE-PSTACK", "ACL2-USER", "ACL2"),
("VERIFY", "ACL2-USER", "ACL2"),
("VERIFY-GUARDS", "ACL2-USER", "ACL2"),
("VERIFY-TERMINATION", "ACL2-USER", "ACL2"),
("W", "ACL2-USER", "ACL2"),
("WARNING!", "ACL2-USER", "ACL2"),
("WET", "ACL2-USER", "ACL2"),
("WITH-OUTPUT", "ACL2-USER", "ACL2"),
("WORLD", "ACL2-USER", "ACL2"),
("WORLDP", "ACL2-USER", "ACL2"),
("WORLDP-FORWARD-TO-ASSOC-EQ-EQUAL-ALISTP", "ACL2-USER", "ACL2"),
("WORMHOLE", "ACL2-USER", "ACL2"),
("WORMHOLE1", "ACL2-USER", "ACL2"),
("WRITABLE-FILE-LISTP", "ACL2-USER", "ACL2"),
("WRITABLE-FILE-LISTP-FORWARD-TO-TRUE-LIST-LISTP", "ACL2-USER", "ACL2"),
("WRITABLE-FILE-LISTP1", "ACL2-USER", "ACL2"),
("WRITABLE-FILE-LISTP1-FORWARD-TO-TRUE-LISTP-AND-CONSP", "ACL2-USER",
"ACL2"),
("WRITE-BYTE$", "ACL2-USER", "ACL2"),
("WRITEABLE-FILES", "ACL2-USER", "ACL2"),
("WRITEABLE-FILES-P", "ACL2-USER", "ACL2"),
("WRITEABLE-FILES-P-FORWARD-TO-WRITABLE-FILE-LISTP", "ACL2-USER", "ACL2"),
("WRITTEN-FILE", "ACL2-USER", "ACL2"),
("WRITTEN-FILE-FORWARD-TO-TRUE-LISTP-AND-CONSP", "ACL2-USER", "ACL2"),
("WRITTEN-FILE-LISTP", "ACL2-USER", "ACL2"),
("WRITTEN-FILE-LISTP-FORWARD-TO-TRUE-LIST-LISTP-AND-ALISTP", "ACL2-USER",
"ACL2"),
("WRITTEN-FILES", "ACL2-USER", "ACL2"),
("WRITTEN-FILES-P", "ACL2-USER", "ACL2"),
("WRITTEN-FILES-P-FORWARD-TO-WRITTEN-FILE-LISTP", "ACL2-USER", "ACL2"),
("XARGS", "ACL2-USER", "ACL2"),
("XXXJOIN", "ACL2-USER", "ACL2"),
("ZERO", "ACL2-USER", "ACL2"),
("ZIP", "ACL2-USER", "ACL2"),
("ZP", "ACL2-USER", "ACL2"),
("&ALLOW-OTHER-KEYS", "ACL2-USER", "COMMON-LISP"),
("*PRINT-MISER-WIDTH*", "ACL2-USER", "COMMON-LISP"),
("&AUX", "ACL2-USER", "COMMON-LISP"),
("*PRINT-PPRINT-DISPATCH*", "ACL2-USER", "COMMON-LISP"),
("&BODY", "ACL2-USER", "COMMON-LISP"),
("*PRINT-PRETTY*", "ACL2-USER", "COMMON-LISP"),
("&ENVIRONMENT", "ACL2-USER", "COMMON-LISP"),
("*PRINT-RADIX*", "ACL2-USER", "COMMON-LISP"),
("&KEY", "ACL2-USER", "COMMON-LISP"),
("*PRINT-READABLY*", "ACL2-USER", "COMMON-LISP"),
("&OPTIONAL", "ACL2-USER", "COMMON-LISP"),
("*PRINT-RIGHT-MARGIN*", "ACL2-USER", "COMMON-LISP"),
("&REST", "ACL2-USER", "COMMON-LISP"),
("*QUERY-IO*", "ACL2-USER", "COMMON-LISP"),
("&WHOLE", "ACL2-USER", "COMMON-LISP"),
("*RANDOM-STATE*", "ACL2-USER", "COMMON-LISP"),
("*", "ACL2-USER", "COMMON-LISP"),
("*READ-BASE*", "ACL2-USER", "COMMON-LISP"),
("**", "ACL2-USER", "COMMON-LISP"),
("*READ-DEFAULT-FLOAT-FORMAT*", "ACL2-USER", "COMMON-LISP"),
("***", "ACL2-USER", "COMMON-LISP"),
("*READ-EVAL*", "ACL2-USER", "COMMON-LISP"),
("*BREAK-ON-SIGNALS*", "ACL2-USER", "COMMON-LISP"),
("*READ-SUPPRESS*", "ACL2-USER", "COMMON-LISP"),
("*COMPILE-FILE-PATHNAME*", "ACL2-USER", "COMMON-LISP"),
("*READTABLE*", "ACL2-USER", "COMMON-LISP"),
("*COMPILE-FILE-TRUENAME*", "ACL2-USER", "COMMON-LISP"),
("*STANDARD-INPUT*", "ACL2-USER", "COMMON-LISP"),
("*COMPILE-PRINT*", "ACL2-USER", "COMMON-LISP"),
("*STANDARD-OUTPUT*", "ACL2-USER", "COMMON-LISP"),
("*COMPILE-VERBOSE*", "ACL2-USER", "COMMON-LISP"),
("*TERMINAL-IO*", "ACL2-USER", "COMMON-LISP"),
("*DEBUG-IO*", "ACL2-USER", "COMMON-LISP"),
("*TRACE-OUTPUT*", "ACL2-USER", "COMMON-LISP"),
("*DEBUGGER-HOOK*", "ACL2-USER", "COMMON-LISP"),
("+", "ACL2-USER", "COMMON-LISP"),
("*DEFAULT-PATHNAME-DEFAULTS*", "ACL2-USER", "COMMON-LISP"),
("++", "ACL2-USER", "COMMON-LISP"),
("*ERROR-OUTPUT*", "ACL2-USER", "COMMON-LISP"),
("+++", "ACL2-USER", "COMMON-LISP"),
("*FEATURES*", "ACL2-USER", "COMMON-LISP"),
("-", "ACL2-USER", "COMMON-LISP"),
("*GENSYM-COUNTER*", "ACL2-USER", "COMMON-LISP"),
("/", "ACL2-USER", "COMMON-LISP"),
("*LOAD-PATHNAME*", "ACL2-USER", "COMMON-LISP"),
("//", "ACL2-USER", "COMMON-LISP"),
("*LOAD-PRINT*", "ACL2-USER", "COMMON-LISP"),
("///", "ACL2-USER", "COMMON-LISP"),
("*LOAD-TRUENAME*", "ACL2-USER", "COMMON-LISP"),
("/=", "ACL2-USER", "COMMON-LISP"),
("*LOAD-VERBOSE*", "ACL2-USER", "COMMON-LISP"),
("1+", "ACL2-USER", "COMMON-LISP"),
("*MACROEXPAND-HOOK*", "ACL2-USER", "COMMON-LISP"),
("1-", "ACL2-USER", "COMMON-LISP"),
("*MODULES*", "ACL2-USER", "COMMON-LISP"),
("<", "ACL2-USER", "COMMON-LISP"),
("*PACKAGE*", "ACL2-USER", "COMMON-LISP"),
("<=", "ACL2-USER", "COMMON-LISP"),
("*PRINT-ARRAY*", "ACL2-USER", "COMMON-LISP"),
("=", "ACL2-USER", "COMMON-LISP"),
("*PRINT-BASE*", "ACL2-USER", "COMMON-LISP"),
(">", "ACL2-USER", "COMMON-LISP"),
("*PRINT-CASE*", "ACL2-USER", "COMMON-LISP"),
(">=", "ACL2-USER", "COMMON-LISP"),
("*PRINT-CIRCLE*", "ACL2-USER", "COMMON-LISP"),
("ABORT", "ACL2-USER", "COMMON-LISP"),
("*PRINT-ESCAPE*", "ACL2-USER", "COMMON-LISP"),
("ABS", "ACL2-USER", "COMMON-LISP"),
("*PRINT-GENSYM*", "ACL2-USER", "COMMON-LISP"),
("ACONS", "ACL2-USER", "COMMON-LISP"),
("*PRINT-LENGTH*", "ACL2-USER", "COMMON-LISP"),
("ACOS", "ACL2-USER", "COMMON-LISP"),
("*PRINT-LEVEL*", "ACL2-USER", "COMMON-LISP"),
("ACOSH", "ACL2-USER", "COMMON-LISP"),
("*PRINT-LINES*", "ACL2-USER", "COMMON-LISP"),
("ADD-METHOD", "ACL2-USER", "COMMON-LISP"),
("ADJOIN", "ACL2-USER", "COMMON-LISP"),
("ATOM", "ACL2-USER", "COMMON-LISP"),
("BOUNDP", "ACL2-USER", "COMMON-LISP"),
("ADJUST-ARRAY", "ACL2-USER", "COMMON-LISP"),
("BASE-CHAR", "ACL2-USER", "COMMON-LISP"),
("BREAK", "ACL2-USER", "COMMON-LISP"),
("ADJUSTABLE-ARRAY-P", "ACL2-USER", "COMMON-LISP"),
("BASE-STRING", "ACL2-USER", "COMMON-LISP"),
("BROADCAST-STREAM", "ACL2-USER", "COMMON-LISP"),
("ALLOCATE-INSTANCE", "ACL2-USER", "COMMON-LISP"),
("BIGNUM", "ACL2-USER", "COMMON-LISP"),
("BROADCAST-STREAM-STREAMS", "ACL2-USER", "COMMON-LISP"),
("ALPHA-CHAR-P", "ACL2-USER", "COMMON-LISP"),
("BIT", "ACL2-USER", "COMMON-LISP"),
("BUILT-IN-CLASS", "ACL2-USER", "COMMON-LISP"),
("ALPHANUMERICP", "ACL2-USER", "COMMON-LISP"),
("BIT-AND", "ACL2-USER", "COMMON-LISP"),
("BUTLAST", "ACL2-USER", "COMMON-LISP"),
("AND", "ACL2-USER", "COMMON-LISP"),
("BIT-ANDC1", "ACL2-USER", "COMMON-LISP"),
("BYTE", "ACL2-USER", "COMMON-LISP"),
("APPEND", "ACL2-USER", "COMMON-LISP"),
("BIT-ANDC2", "ACL2-USER", "COMMON-LISP"),
("BYTE-POSITION", "ACL2-USER", "COMMON-LISP"),
("APPLY", "ACL2-USER", "COMMON-LISP"),
("BIT-EQV", "ACL2-USER", "COMMON-LISP"),
("BYTE-SIZE", "ACL2-USER", "COMMON-LISP"),
("APROPOS", "ACL2-USER", "COMMON-LISP"),
("BIT-IOR", "ACL2-USER", "COMMON-LISP"),
("CAAAAR", "ACL2-USER", "COMMON-LISP"),
("APROPOS-LIST", "ACL2-USER", "COMMON-LISP"),
("BIT-NAND", "ACL2-USER", "COMMON-LISP"),
("CAAADR", "ACL2-USER", "COMMON-LISP"),
("AREF", "ACL2-USER", "COMMON-LISP"),
("BIT-NOR", "ACL2-USER", "COMMON-LISP"),
("CAAAR", "ACL2-USER", "COMMON-LISP"),
("ARITHMETIC-ERROR", "ACL2-USER", "COMMON-LISP"),
("BIT-NOT", "ACL2-USER", "COMMON-LISP"),
("CAADAR", "ACL2-USER", "COMMON-LISP"),
("ARITHMETIC-ERROR-OPERANDS", "ACL2-USER", "COMMON-LISP"),
("BIT-ORC1", "ACL2-USER", "COMMON-LISP"),
("CAADDR", "ACL2-USER", "COMMON-LISP"),
("ARITHMETIC-ERROR-OPERATION", "ACL2-USER", "COMMON-LISP"),
("BIT-ORC2", "ACL2-USER", "COMMON-LISP"),
("CAADR", "ACL2-USER", "COMMON-LISP"),
("ARRAY", "ACL2-USER", "COMMON-LISP"),
("BIT-VECTOR", "ACL2-USER", "COMMON-LISP"),
("CAAR", "ACL2-USER", "COMMON-LISP"),
("ARRAY-DIMENSION", "ACL2-USER", "COMMON-LISP"),
("BIT-VECTOR-P", "ACL2-USER", "COMMON-LISP"),
("CADAAR", "ACL2-USER", "COMMON-LISP"),
("ARRAY-DIMENSION-LIMIT", "ACL2-USER", "COMMON-LISP"),
("BIT-XOR", "ACL2-USER", "COMMON-LISP"),
("CADADR", "ACL2-USER", "COMMON-LISP"),
("ARRAY-DIMENSIONS", "ACL2-USER", "COMMON-LISP"),
("BLOCK", "ACL2-USER", "COMMON-LISP"),
("CADAR", "ACL2-USER", "COMMON-LISP"),
("ARRAY-DISPLACEMENT", "ACL2-USER", "COMMON-LISP"),
("BOOLE", "ACL2-USER", "COMMON-LISP"),
("CADDAR", "ACL2-USER", "COMMON-LISP"),
("ARRAY-ELEMENT-TYPE", "ACL2-USER", "COMMON-LISP"),
("BOOLE-1", "ACL2-USER", "COMMON-LISP"),
("CADDDR", "ACL2-USER", "COMMON-LISP"),
("ARRAY-HAS-FILL-POINTER-P", "ACL2-USER", "COMMON-LISP"),
("BOOLE-2", "ACL2-USER", "COMMON-LISP"),
("CADDR", "ACL2-USER", "COMMON-LISP"),
("ARRAY-IN-BOUNDS-P", "ACL2-USER", "COMMON-LISP"),
("BOOLE-AND", "ACL2-USER", "COMMON-LISP"),
("CADR", "ACL2-USER", "COMMON-LISP"),
("ARRAY-RANK", "ACL2-USER", "COMMON-LISP"),
("BOOLE-ANDC1", "ACL2-USER", "COMMON-LISP"),
("CALL-ARGUMENTS-LIMIT", "ACL2-USER", "COMMON-LISP"),
("ARRAY-RANK-LIMIT", "ACL2-USER", "COMMON-LISP"),
("BOOLE-ANDC2", "ACL2-USER", "COMMON-LISP"),
("CALL-METHOD", "ACL2-USER", "COMMON-LISP"),
("ARRAY-ROW-MAJOR-INDEX", "ACL2-USER", "COMMON-LISP"),
("BOOLE-C1", "ACL2-USER", "COMMON-LISP"),
("CALL-NEXT-METHOD", "ACL2-USER", "COMMON-LISP"),
("ARRAY-TOTAL-SIZE", "ACL2-USER", "COMMON-LISP"),
("BOOLE-C2", "ACL2-USER", "COMMON-LISP"),
("CAR", "ACL2-USER", "COMMON-LISP"),
("ARRAY-TOTAL-SIZE-LIMIT", "ACL2-USER", "COMMON-LISP"),
("BOOLE-CLR", "ACL2-USER", "COMMON-LISP"),
("CASE", "ACL2-USER", "COMMON-LISP"),
("ARRAYP", "ACL2-USER", "COMMON-LISP"),
("BOOLE-EQV", "ACL2-USER", "COMMON-LISP"),
("CATCH", "ACL2-USER", "COMMON-LISP"),
("ASH", "ACL2-USER", "COMMON-LISP"),
("BOOLE-IOR", "ACL2-USER", "COMMON-LISP"),
("CCASE", "ACL2-USER", "COMMON-LISP"),
("ASIN", "ACL2-USER", "COMMON-LISP"),
("BOOLE-NAND", "ACL2-USER", "COMMON-LISP"),
("CDAAAR", "ACL2-USER", "COMMON-LISP"),
("ASINH", "ACL2-USER", "COMMON-LISP"),
("BOOLE-NOR", "ACL2-USER", "COMMON-LISP"),
("CDAADR", "ACL2-USER", "COMMON-LISP"),
("ASSERT", "ACL2-USER", "COMMON-LISP"),
("BOOLE-ORC1", "ACL2-USER", "COMMON-LISP"),
("CDAAR", "ACL2-USER", "COMMON-LISP"),
("ASSOC", "ACL2-USER", "COMMON-LISP"),
("BOOLE-ORC2", "ACL2-USER", "COMMON-LISP"),
("CDADAR", "ACL2-USER", "COMMON-LISP"),
("ASSOC-IF", "ACL2-USER", "COMMON-LISP"),
("BOOLE-SET", "ACL2-USER", "COMMON-LISP"),
("CDADDR", "ACL2-USER", "COMMON-LISP"),
("ASSOC-IF-NOT", "ACL2-USER", "COMMON-LISP"),
("BOOLE-XOR", "ACL2-USER", "COMMON-LISP"),
("CDADR", "ACL2-USER", "COMMON-LISP"),
("ATAN", "ACL2-USER", "COMMON-LISP"),
("BOOLEAN", "ACL2-USER", "COMMON-LISP"),
("CDAR", "ACL2-USER", "COMMON-LISP"),
("ATANH", "ACL2-USER", "COMMON-LISP"),
("BOTH-CASE-P", "ACL2-USER", "COMMON-LISP"),
("CDDAAR", "ACL2-USER", "COMMON-LISP"),
("CDDADR", "ACL2-USER", "COMMON-LISP"),
("CLEAR-INPUT", "ACL2-USER", "COMMON-LISP"),
("COPY-TREE", "ACL2-USER", "COMMON-LISP"),
("CDDAR", "ACL2-USER", "COMMON-LISP"),
("CLEAR-OUTPUT", "ACL2-USER", "COMMON-LISP"),
("COS", "ACL2-USER", "COMMON-LISP"),
("CDDDAR", "ACL2-USER", "COMMON-LISP"),
("CLOSE", "ACL2-USER", "COMMON-LISP"),
("COSH", "ACL2-USER", "COMMON-LISP"),
("CDDDDR", "ACL2-USER", "COMMON-LISP"),
("CLRHASH", "ACL2-USER", "COMMON-LISP"),
("COUNT", "ACL2-USER", "COMMON-LISP"),
("CDDDR", "ACL2-USER", "COMMON-LISP"),
("CODE-CHAR", "ACL2-USER", "COMMON-LISP"),
("COUNT-IF", "ACL2-USER", "COMMON-LISP"),
("CDDR", "ACL2-USER", "COMMON-LISP"),
("COERCE", "ACL2-USER", "COMMON-LISP"),
("COUNT-IF-NOT", "ACL2-USER", "COMMON-LISP"),
("CDR", "ACL2-USER", "COMMON-LISP"),
("COMPILATION-SPEED", "ACL2-USER", "COMMON-LISP"),
("CTYPECASE", "ACL2-USER", "COMMON-LISP"),
("CEILING", "ACL2-USER", "COMMON-LISP"),
("COMPILE", "ACL2-USER", "COMMON-LISP"),
("DEBUG", "ACL2-USER", "COMMON-LISP"),
("CELL-ERROR", "ACL2-USER", "COMMON-LISP"),
("COMPILE-FILE", "ACL2-USER", "COMMON-LISP"),
("DECF", "ACL2-USER", "COMMON-LISP"),
("CELL-ERROR-NAME", "ACL2-USER", "COMMON-LISP"),
("COMPILE-FILE-PATHNAME", "ACL2-USER", "COMMON-LISP"),
("DECLAIM", "ACL2-USER", "COMMON-LISP"),
("CERROR", "ACL2-USER", "COMMON-LISP"),
("COMPILED-FUNCTION", "ACL2-USER", "COMMON-LISP"),
("DECLARATION", "ACL2-USER", "COMMON-LISP"),
("CHANGE-CLASS", "ACL2-USER", "COMMON-LISP"),
("COMPILED-FUNCTION-P", "ACL2-USER", "COMMON-LISP"),
("DECLARE", "ACL2-USER", "COMMON-LISP"),
("CHAR", "ACL2-USER", "COMMON-LISP"),
("COMPILER-MACRO", "ACL2-USER", "COMMON-LISP"),
("DECODE-FLOAT", "ACL2-USER", "COMMON-LISP"),
("CHAR-CODE", "ACL2-USER", "COMMON-LISP"),
("COMPILER-MACRO-FUNCTION", "ACL2-USER", "COMMON-LISP"),
("DECODE-UNIVERSAL-TIME", "ACL2-USER", "COMMON-LISP"),
("CHAR-CODE-LIMIT", "ACL2-USER", "COMMON-LISP"),
("COMPLEMENT", "ACL2-USER", "COMMON-LISP"),
("DEFCLASS", "ACL2-USER", "COMMON-LISP"),
("CHAR-DOWNCASE", "ACL2-USER", "COMMON-LISP"),
("COMPLEX", "ACL2-USER", "COMMON-LISP"),
("DEFCONSTANT", "ACL2-USER", "COMMON-LISP"),
("CHAR-EQUAL", "ACL2-USER", "COMMON-LISP"),
("COMPLEXP", "ACL2-USER", "COMMON-LISP"),
("DEFGENERIC", "ACL2-USER", "COMMON-LISP"),
("CHAR-GREATERP", "ACL2-USER", "COMMON-LISP"),
("COMPUTE-APPLICABLE-METHODS", "ACL2-USER", "COMMON-LISP"),
("DEFINE-COMPILER-MACRO", "ACL2-USER", "COMMON-LISP"),
("CHAR-INT", "ACL2-USER", "COMMON-LISP"),
("COMPUTE-RESTARTS", "ACL2-USER", "COMMON-LISP"),
("DEFINE-CONDITION", "ACL2-USER", "COMMON-LISP"),
("CHAR-LESSP", "ACL2-USER", "COMMON-LISP"),
("CONCATENATE", "ACL2-USER", "COMMON-LISP"),
("DEFINE-METHOD-COMBINATION", "ACL2-USER", "COMMON-LISP"),
("CHAR-NAME", "ACL2-USER", "COMMON-LISP"),
("CONCATENATED-STREAM", "ACL2-USER", "COMMON-LISP"),
("DEFINE-MODIFY-MACRO", "ACL2-USER", "COMMON-LISP"),
("CHAR-NOT-EQUAL", "ACL2-USER", "COMMON-LISP"),
("CONCATENATED-STREAM-STREAMS", "ACL2-USER", "COMMON-LISP"),
("DEFINE-SETF-EXPANDER", "ACL2-USER", "COMMON-LISP"),
("CHAR-NOT-GREATERP", "ACL2-USER", "COMMON-LISP"),
("COND", "ACL2-USER", "COMMON-LISP"),
("DEFINE-SYMBOL-MACRO", "ACL2-USER", "COMMON-LISP"),
("CHAR-NOT-LESSP", "ACL2-USER", "COMMON-LISP"),
("CONDITION", "ACL2-USER", "COMMON-LISP"),
("DEFMACRO", "ACL2-USER", "COMMON-LISP"),
("CHAR-UPCASE", "ACL2-USER", "COMMON-LISP"),
("CONJUGATE", "ACL2-USER", "COMMON-LISP"),
("DEFMETHOD", "ACL2-USER", "COMMON-LISP"),
("CHAR/=", "ACL2-USER", "COMMON-LISP"),
("CONS", "ACL2-USER", "COMMON-LISP"),
("DEFPACKAGE", "ACL2-USER", "COMMON-LISP"),
("CHAR<", "ACL2-USER", "COMMON-LISP"),
("CONSP", "ACL2-USER", "COMMON-LISP"),
("DEFPARAMETER", "ACL2-USER", "COMMON-LISP"),
("CHAR<=", "ACL2-USER", "COMMON-LISP"),
("CONSTANTLY", "ACL2-USER", "COMMON-LISP"),
("DEFSETF", "ACL2-USER", "COMMON-LISP"),
("CHAR=", "ACL2-USER", "COMMON-LISP"),
("CONSTANTP", "ACL2-USER", "COMMON-LISP"),
("DEFSTRUCT", "ACL2-USER", "COMMON-LISP"),
("CHAR>", "ACL2-USER", "COMMON-LISP"),
("CONTINUE", "ACL2-USER", "COMMON-LISP"),
("DEFTYPE", "ACL2-USER", "COMMON-LISP"),
("CHAR>=", "ACL2-USER", "COMMON-LISP"),
("CONTROL-ERROR", "ACL2-USER", "COMMON-LISP"),
("DEFUN", "ACL2-USER", "COMMON-LISP"),
("CHARACTER", "ACL2-USER", "COMMON-LISP"),
("COPY-ALIST", "ACL2-USER", "COMMON-LISP"),
("DEFVAR", "ACL2-USER", "COMMON-LISP"),
("CHARACTERP", "ACL2-USER", "COMMON-LISP"),
("COPY-LIST", "ACL2-USER", "COMMON-LISP"),
("DELETE", "ACL2-USER", "COMMON-LISP"),
("CHECK-TYPE", "ACL2-USER", "COMMON-LISP"),
("COPY-PPRINT-DISPATCH", "ACL2-USER", "COMMON-LISP"),
("DELETE-DUPLICATES", "ACL2-USER", "COMMON-LISP"),
("CIS", "ACL2-USER", "COMMON-LISP"),
("COPY-READTABLE", "ACL2-USER", "COMMON-LISP"),
("DELETE-FILE", "ACL2-USER", "COMMON-LISP"),
("CLASS", "ACL2-USER", "COMMON-LISP"),
("COPY-SEQ", "ACL2-USER", "COMMON-LISP"),
("DELETE-IF", "ACL2-USER", "COMMON-LISP"),
("CLASS-NAME", "ACL2-USER", "COMMON-LISP"),
("COPY-STRUCTURE", "ACL2-USER", "COMMON-LISP"),
("DELETE-IF-NOT", "ACL2-USER", "COMMON-LISP"),
("CLASS-OF", "ACL2-USER", "COMMON-LISP"),
("COPY-SYMBOL", "ACL2-USER", "COMMON-LISP"),
("DELETE-PACKAGE", "ACL2-USER", "COMMON-LISP"),
("DENOMINATOR", "ACL2-USER", "COMMON-LISP"),
("EQ", "ACL2-USER", "COMMON-LISP"),
("DEPOSIT-FIELD", "ACL2-USER", "COMMON-LISP"),
("EQL", "ACL2-USER", "COMMON-LISP"),
("DESCRIBE", "ACL2-USER", "COMMON-LISP"),
("EQUAL", "ACL2-USER", "COMMON-LISP"),
("DESCRIBE-OBJECT", "ACL2-USER", "COMMON-LISP"),
("EQUALP", "ACL2-USER", "COMMON-LISP"),
("DESTRUCTURING-BIND", "ACL2-USER", "COMMON-LISP"),
("ERROR", "ACL2-USER", "COMMON-LISP"),
("DIGIT-CHAR", "ACL2-USER", "COMMON-LISP"),
("ETYPECASE", "ACL2-USER", "COMMON-LISP"),
("DIGIT-CHAR-P", "ACL2-USER", "COMMON-LISP"),
("EVAL", "ACL2-USER", "COMMON-LISP"),
("DIRECTORY", "ACL2-USER", "COMMON-LISP"),
("EVAL-WHEN", "ACL2-USER", "COMMON-LISP"),
("DIRECTORY-NAMESTRING", "ACL2-USER", "COMMON-LISP"),
("EVENP", "ACL2-USER", "COMMON-LISP"),
("DISASSEMBLE", "ACL2-USER", "COMMON-LISP"),
("EVERY", "ACL2-USER", "COMMON-LISP"),
("DIVISION-BY-ZERO", "ACL2-USER", "COMMON-LISP"),
("EXP", "ACL2-USER", "COMMON-LISP"),
("DO", "ACL2-USER", "COMMON-LISP"),
("EXPORT", "ACL2-USER", "COMMON-LISP"),
("DO*", "ACL2-USER", "COMMON-LISP"),
("EXPT", "ACL2-USER", "COMMON-LISP"),
("DO-ALL-SYMBOLS", "ACL2-USER", "COMMON-LISP"),
("EXTENDED-CHAR", "ACL2-USER", "COMMON-LISP"),
("DO-EXTERNAL-SYMBOLS", "ACL2-USER", "COMMON-LISP"),
("FBOUNDP", "ACL2-USER", "COMMON-LISP"),
("DO-SYMBOLS", "ACL2-USER", "COMMON-LISP"),
("FCEILING", "ACL2-USER", "COMMON-LISP"),
("DOCUMENTATION", "ACL2-USER", "COMMON-LISP"),
("FDEFINITION", "ACL2-USER", "COMMON-LISP"),
("DOLIST", "ACL2-USER", "COMMON-LISP"),
("FFLOOR", "ACL2-USER", "COMMON-LISP"),
("DOTIMES", "ACL2-USER", "COMMON-LISP"),
("FIFTH", "ACL2-USER", "COMMON-LISP"),
("DOUBLE-FLOAT", "ACL2-USER", "COMMON-LISP"),
("FILE-AUTHOR", "ACL2-USER", "COMMON-LISP"),
("DOUBLE-FLOAT-EPSILON", "ACL2-USER", "COMMON-LISP"),
("FILE-ERROR", "ACL2-USER", "COMMON-LISP"),
("DOUBLE-FLOAT-NEGATIVE-EPSILON", "ACL2-USER", "COMMON-LISP"),
("FILE-ERROR-PATHNAME", "ACL2-USER", "COMMON-LISP"),
("DPB", "ACL2-USER", "COMMON-LISP"),
("FILE-LENGTH", "ACL2-USER", "COMMON-LISP"),
("DRIBBLE", "ACL2-USER", "COMMON-LISP"),
("FILE-NAMESTRING", "ACL2-USER", "COMMON-LISP"),
("DYNAMIC-EXTENT", "ACL2-USER", "COMMON-LISP"),
("FILE-POSITION", "ACL2-USER", "COMMON-LISP"),
("ECASE", "ACL2-USER", "COMMON-LISP"),
("FILE-STREAM", "ACL2-USER", "COMMON-LISP"),
("ECHO-STREAM", "ACL2-USER", "COMMON-LISP"),
("FILE-STRING-LENGTH", "ACL2-USER", "COMMON-LISP"),
("ECHO-STREAM-INPUT-STREAM", "ACL2-USER", "COMMON-LISP"),
("FILE-WRITE-DATE", "ACL2-USER", "COMMON-LISP"),
("ECHO-STREAM-OUTPUT-STREAM", "ACL2-USER", "COMMON-LISP"),
("FILL", "ACL2-USER", "COMMON-LISP"),
("ED", "ACL2-USER", "COMMON-LISP"),
("FILL-POINTER", "ACL2-USER", "COMMON-LISP"),
("EIGHTH", "ACL2-USER", "COMMON-LISP"),
("FIND", "ACL2-USER", "COMMON-LISP"),
("ELT", "ACL2-USER", "COMMON-LISP"),
("FIND-ALL-SYMBOLS", "ACL2-USER", "COMMON-LISP"),
("ENCODE-UNIVERSAL-TIME", "ACL2-USER", "COMMON-LISP"),
("FIND-CLASS", "ACL2-USER", "COMMON-LISP"),
("END-OF-FILE", "ACL2-USER", "COMMON-LISP"),
("FIND-IF", "ACL2-USER", "COMMON-LISP"),
("ENDP", "ACL2-USER", "COMMON-LISP"),
("FIND-IF-NOT", "ACL2-USER", "COMMON-LISP"),
("ENOUGH-NAMESTRING", "ACL2-USER", "COMMON-LISP"),
("FIND-METHOD", "ACL2-USER", "COMMON-LISP"),
("ENSURE-DIRECTORIES-EXIST", "ACL2-USER", "COMMON-LISP"),
("FIND-PACKAGE", "ACL2-USER", "COMMON-LISP"),
("ENSURE-GENERIC-FUNCTION", "ACL2-USER", "COMMON-LISP"),
("FIND-RESTART", "ACL2-USER", "COMMON-LISP"),
("FIND-SYMBOL", "ACL2-USER", "COMMON-LISP"),
("GET-INTERNAL-RUN-TIME", "ACL2-USER", "COMMON-LISP"),
("FINISH-OUTPUT", "ACL2-USER", "COMMON-LISP"),
("GET-MACRO-CHARACTER", "ACL2-USER", "COMMON-LISP"),
("FIRST", "ACL2-USER", "COMMON-LISP"),
("GET-OUTPUT-STREAM-STRING", "ACL2-USER", "COMMON-LISP"),
("FIXNUM", "ACL2-USER", "COMMON-LISP"),
("GET-PROPERTIES", "ACL2-USER", "COMMON-LISP"),
("FLET", "ACL2-USER", "COMMON-LISP"),
("GET-SETF-EXPANSION", "ACL2-USER", "COMMON-LISP"),
("FLOAT", "ACL2-USER", "COMMON-LISP"),
("GET-UNIVERSAL-TIME", "ACL2-USER", "COMMON-LISP"),
("FLOAT-DIGITS", "ACL2-USER", "COMMON-LISP"),
("GETF", "ACL2-USER", "COMMON-LISP"),
("FLOAT-PRECISION", "ACL2-USER", "COMMON-LISP"),
("GETHASH", "ACL2-USER", "COMMON-LISP"),
("FLOAT-RADIX", "ACL2-USER", "COMMON-LISP"),
("GO", "ACL2-USER", "COMMON-LISP"),
("FLOAT-SIGN", "ACL2-USER", "COMMON-LISP"),
("GRAPHIC-CHAR-P", "ACL2-USER", "COMMON-LISP"),
("FLOATING-POINT-INEXACT", "ACL2-USER", "COMMON-LISP"),
("HANDLER-BIND", "ACL2-USER", "COMMON-LISP"),
("FLOATING-POINT-INVALID-OPERATION", "ACL2-USER", "COMMON-LISP"),
("HANDLER-CASE", "ACL2-USER", "COMMON-LISP"),
("FLOATING-POINT-OVERFLOW", "ACL2-USER", "COMMON-LISP"),
("HASH-TABLE", "ACL2-USER", "COMMON-LISP"),
("FLOATING-POINT-UNDERFLOW", "ACL2-USER", "COMMON-LISP"),
("HASH-TABLE-COUNT", "ACL2-USER", "COMMON-LISP"),
("FLOATP", "ACL2-USER", "COMMON-LISP"),
("HASH-TABLE-P", "ACL2-USER", "COMMON-LISP"),
("FLOOR", "ACL2-USER", "COMMON-LISP"),
("HASH-TABLE-REHASH-SIZE", "ACL2-USER", "COMMON-LISP"),
("FMAKUNBOUND", "ACL2-USER", "COMMON-LISP"),
("HASH-TABLE-REHASH-THRESHOLD", "ACL2-USER", "COMMON-LISP"),
("FORCE-OUTPUT", "ACL2-USER", "COMMON-LISP"),
("HASH-TABLE-SIZE", "ACL2-USER", "COMMON-LISP"),
("FORMAT", "ACL2-USER", "COMMON-LISP"),
("HASH-TABLE-TEST", "ACL2-USER", "COMMON-LISP"),
("FORMATTER", "ACL2-USER", "COMMON-LISP"),
("HOST-NAMESTRING", "ACL2-USER", "COMMON-LISP"),
("FOURTH", "ACL2-USER", "COMMON-LISP"),
("IDENTITY", "ACL2-USER", "COMMON-LISP"),
("FRESH-LINE", "ACL2-USER", "COMMON-LISP"),
("IF", "ACL2-USER", "COMMON-LISP"),
("FROUND", "ACL2-USER", "COMMON-LISP"),
("IGNORABLE", "ACL2-USER", "COMMON-LISP"),
("FTRUNCATE", "ACL2-USER", "COMMON-LISP"),
("IGNORE", "ACL2-USER", "COMMON-LISP"),
("FTYPE", "ACL2-USER", "COMMON-LISP"),
("IGNORE-ERRORS", "ACL2-USER", "COMMON-LISP"),
("FUNCALL", "ACL2-USER", "COMMON-LISP"),
("IMAGPART", "ACL2-USER", "COMMON-LISP"),
("FUNCTION", "ACL2-USER", "COMMON-LISP"),
("IMPORT", "ACL2-USER", "COMMON-LISP"),
("FUNCTION-KEYWORDS", "ACL2-USER", "COMMON-LISP"),
("IN-PACKAGE", "ACL2-USER", "COMMON-LISP"),
("FUNCTION-LAMBDA-EXPRESSION", "ACL2-USER", "COMMON-LISP"),
("INCF", "ACL2-USER", "COMMON-LISP"),
("FUNCTIONP", "ACL2-USER", "COMMON-LISP"),
("INITIALIZE-INSTANCE", "ACL2-USER", "COMMON-LISP"),
("GCD", "ACL2-USER", "COMMON-LISP"),
("INLINE", "ACL2-USER", "COMMON-LISP"),
("GENERIC-FUNCTION", "ACL2-USER", "COMMON-LISP"),
("INPUT-STREAM-P", "ACL2-USER", "COMMON-LISP"),
("GENSYM", "ACL2-USER", "COMMON-LISP"),
("INSPECT", "ACL2-USER", "COMMON-LISP"),
("GENTEMP", "ACL2-USER", "COMMON-LISP"),
("INTEGER", "ACL2-USER", "COMMON-LISP"),
("GET", "ACL2-USER", "COMMON-LISP"),
("INTEGER-DECODE-FLOAT", "ACL2-USER", "COMMON-LISP"),
("GET-DECODED-TIME", "ACL2-USER", "COMMON-LISP"),
("INTEGER-LENGTH", "ACL2-USER", "COMMON-LISP"),
("GET-DISPATCH-MACRO-CHARACTER", "ACL2-USER", "COMMON-LISP"),
("INTEGERP", "ACL2-USER", "COMMON-LISP"),
("GET-INTERNAL-REAL-TIME", "ACL2-USER", "COMMON-LISP"),
("INTERACTIVE-STREAM-P", "ACL2-USER", "COMMON-LISP"),
("INTERN", "ACL2-USER", "COMMON-LISP"),
("LISP-IMPLEMENTATION-TYPE", "ACL2-USER", "COMMON-LISP"),
("INTERNAL-TIME-UNITS-PER-SECOND", "ACL2-USER", "COMMON-LISP"),
("LISP-IMPLEMENTATION-VERSION", "ACL2-USER", "COMMON-LISP"),
("INTERSECTION", "ACL2-USER", "COMMON-LISP"),
("LIST", "ACL2-USER", "COMMON-LISP"),
("INVALID-METHOD-ERROR", "ACL2-USER", "COMMON-LISP"),
("LIST*", "ACL2-USER", "COMMON-LISP"),
("INVOKE-DEBUGGER", "ACL2-USER", "COMMON-LISP"),
("LIST-ALL-PACKAGES", "ACL2-USER", "COMMON-LISP"),
("INVOKE-RESTART", "ACL2-USER", "COMMON-LISP"),
("LIST-LENGTH", "ACL2-USER", "COMMON-LISP"),
("INVOKE-RESTART-INTERACTIVELY", "ACL2-USER", "COMMON-LISP"),
("LISTEN", "ACL2-USER", "COMMON-LISP"),
("ISQRT", "ACL2-USER", "COMMON-LISP"),
("LISTP", "ACL2-USER", "COMMON-LISP"),
("KEYWORD", "ACL2-USER", "COMMON-LISP"),
("LOAD", "ACL2-USER", "COMMON-LISP"),
("KEYWORDP", "ACL2-USER", "COMMON-LISP"),
("LOAD-LOGICAL-PATHNAME-TRANSLATIONS", "ACL2-USER", "COMMON-LISP"),
("LABELS", "ACL2-USER", "COMMON-LISP"),
("LOAD-TIME-VALUE", "ACL2-USER", "COMMON-LISP"),
("LAMBDA", "ACL2-USER", "COMMON-LISP"),
("LOCALLY", "ACL2-USER", "COMMON-LISP"),
("LAMBDA-LIST-KEYWORDS", "ACL2-USER", "COMMON-LISP"),
("LOG", "ACL2-USER", "COMMON-LISP"),
("LAMBDA-PARAMETERS-LIMIT", "ACL2-USER", "COMMON-LISP"),
("LOGAND", "ACL2-USER", "COMMON-LISP"),
("LAST", "ACL2-USER", "COMMON-LISP"),
("LOGANDC1", "ACL2-USER", "COMMON-LISP"),
("LCM", "ACL2-USER", "COMMON-LISP"),
("LOGANDC2", "ACL2-USER", "COMMON-LISP"),
("LDB", "ACL2-USER", "COMMON-LISP"),
("LOGBITP", "ACL2-USER", "COMMON-LISP"),
("LDB-TEST", "ACL2-USER", "COMMON-LISP"),
("LOGCOUNT", "ACL2-USER", "COMMON-LISP"),
("LDIFF", "ACL2-USER", "COMMON-LISP"),
("LOGEQV", "ACL2-USER", "COMMON-LISP"),
("LEAST-NEGATIVE-DOUBLE-FLOAT", "ACL2-USER", "COMMON-LISP"),
("LOGICAL-PATHNAME", "ACL2-USER", "COMMON-LISP"),
("LEAST-NEGATIVE-LONG-FLOAT", "ACL2-USER", "COMMON-LISP"),
("LOGICAL-PATHNAME-TRANSLATIONS", "ACL2-USER", "COMMON-LISP"),
("LEAST-NEGATIVE-NORMALIZED-DOUBLE-FLOAT", "ACL2-USER", "COMMON-LISP"),
("LOGIOR", "ACL2-USER", "COMMON-LISP"),
("LEAST-NEGATIVE-NORMALIZED-LONG-FLOAT", "ACL2-USER", "COMMON-LISP"),
("LOGNAND", "ACL2-USER", "COMMON-LISP"),
("LEAST-NEGATIVE-NORMALIZED-SHORT-FLOAT", "ACL2-USER", "COMMON-LISP"),
("LOGNOR", "ACL2-USER", "COMMON-LISP"),
("LEAST-NEGATIVE-NORMALIZED-SINGLE-FLOAT", "ACL2-USER", "COMMON-LISP"),
("LOGNOT", "ACL2-USER", "COMMON-LISP"),
("LEAST-NEGATIVE-SHORT-FLOAT", "ACL2-USER", "COMMON-LISP"),
("LOGORC1", "ACL2-USER", "COMMON-LISP"),
("LEAST-NEGATIVE-SINGLE-FLOAT", "ACL2-USER", "COMMON-LISP"),
("LOGORC2", "ACL2-USER", "COMMON-LISP"),
("LEAST-POSITIVE-DOUBLE-FLOAT", "ACL2-USER", "COMMON-LISP"),
("LOGTEST", "ACL2-USER", "COMMON-LISP"),
("LEAST-POSITIVE-LONG-FLOAT", "ACL2-USER", "COMMON-LISP"),
("LOGXOR", "ACL2-USER", "COMMON-LISP"),
("LEAST-POSITIVE-NORMALIZED-DOUBLE-FLOAT", "ACL2-USER", "COMMON-LISP"),
("LONG-FLOAT", "ACL2-USER", "COMMON-LISP"),
("LEAST-POSITIVE-NORMALIZED-LONG-FLOAT", "ACL2-USER", "COMMON-LISP"),
("LONG-FLOAT-EPSILON", "ACL2-USER", "COMMON-LISP"),
("LEAST-POSITIVE-NORMALIZED-SHORT-FLOAT", "ACL2-USER", "COMMON-LISP"),
("LONG-FLOAT-NEGATIVE-EPSILON", "ACL2-USER", "COMMON-LISP"),
("LEAST-POSITIVE-NORMALIZED-SINGLE-FLOAT", "ACL2-USER", "COMMON-LISP"),
("LONG-SITE-NAME", "ACL2-USER", "COMMON-LISP"),
("LEAST-POSITIVE-SHORT-FLOAT", "ACL2-USER", "COMMON-LISP"),
("LOOP", "ACL2-USER", "COMMON-LISP"),
("LEAST-POSITIVE-SINGLE-FLOAT", "ACL2-USER", "COMMON-LISP"),
("LOOP-FINISH", "ACL2-USER", "COMMON-LISP"),
("LENGTH", "ACL2-USER", "COMMON-LISP"),
("LOWER-CASE-P", "ACL2-USER", "COMMON-LISP"),
("LET", "ACL2-USER", "COMMON-LISP"),
("MACHINE-INSTANCE", "ACL2-USER", "COMMON-LISP"),
("LET*", "ACL2-USER", "COMMON-LISP"),
("MACHINE-TYPE", "ACL2-USER", "COMMON-LISP"),
("MACHINE-VERSION", "ACL2-USER", "COMMON-LISP"),
("MASK-FIELD", "ACL2-USER", "COMMON-LISP"),
("MACRO-FUNCTION", "ACL2-USER", "COMMON-LISP"),
("MAX", "ACL2-USER", "COMMON-LISP"),
("MACROEXPAND", "ACL2-USER", "COMMON-LISP"),
("MEMBER", "ACL2-USER", "COMMON-LISP"),
("MACROEXPAND-1", "ACL2-USER", "COMMON-LISP"),
("MEMBER-IF", "ACL2-USER", "COMMON-LISP"),
("MACROLET", "ACL2-USER", "COMMON-LISP"),
("MEMBER-IF-NOT", "ACL2-USER", "COMMON-LISP"),
("MAKE-ARRAY", "ACL2-USER", "COMMON-LISP"),
("MERGE", "ACL2-USER", "COMMON-LISP"),
("MAKE-BROADCAST-STREAM", "ACL2-USER", "COMMON-LISP"),
("MERGE-PATHNAMES", "ACL2-USER", "COMMON-LISP"),
("MAKE-CONCATENATED-STREAM", "ACL2-USER", "COMMON-LISP"),
("METHOD", "ACL2-USER", "COMMON-LISP"),
("MAKE-CONDITION", "ACL2-USER", "COMMON-LISP"),
("METHOD-COMBINATION", "ACL2-USER", "COMMON-LISP"),
("MAKE-DISPATCH-MACRO-CHARACTER", "ACL2-USER", "COMMON-LISP"),
("METHOD-COMBINATION-ERROR", "ACL2-USER", "COMMON-LISP"),
("MAKE-ECHO-STREAM", "ACL2-USER", "COMMON-LISP"),
("METHOD-QUALIFIERS", "ACL2-USER", "COMMON-LISP"),
("MAKE-HASH-TABLE", "ACL2-USER", "COMMON-LISP"),
("MIN", "ACL2-USER", "COMMON-LISP"),
("MAKE-INSTANCE", "ACL2-USER", "COMMON-LISP"),
("MINUSP", "ACL2-USER", "COMMON-LISP"),
("MAKE-INSTANCES-OBSOLETE", "ACL2-USER", "COMMON-LISP"),
("MISMATCH", "ACL2-USER", "COMMON-LISP"),
("MAKE-LIST", "ACL2-USER", "COMMON-LISP"),
("MOD", "ACL2-USER", "COMMON-LISP"),
("MAKE-LOAD-FORM", "ACL2-USER", "COMMON-LISP"),
("MOST-NEGATIVE-DOUBLE-FLOAT", "ACL2-USER", "COMMON-LISP"),
("MAKE-LOAD-FORM-SAVING-SLOTS", "ACL2-USER", "COMMON-LISP"),
("MOST-NEGATIVE-FIXNUM", "ACL2-USER", "COMMON-LISP"),
("MAKE-METHOD", "ACL2-USER", "COMMON-LISP"),
("MOST-NEGATIVE-LONG-FLOAT", "ACL2-USER", "COMMON-LISP"),
("MAKE-PACKAGE", "ACL2-USER", "COMMON-LISP"),
("MOST-NEGATIVE-SHORT-FLOAT", "ACL2-USER", "COMMON-LISP"),
("MAKE-PATHNAME", "ACL2-USER", "COMMON-LISP"),
("MOST-NEGATIVE-SINGLE-FLOAT", "ACL2-USER", "COMMON-LISP"),
("MAKE-RANDOM-STATE", "ACL2-USER", "COMMON-LISP"),
("MOST-POSITIVE-DOUBLE-FLOAT", "ACL2-USER", "COMMON-LISP"),
("MAKE-SEQUENCE", "ACL2-USER", "COMMON-LISP"),
("MOST-POSITIVE-FIXNUM", "ACL2-USER", "COMMON-LISP"),
("MAKE-STRING", "ACL2-USER", "COMMON-LISP"),
("MOST-POSITIVE-LONG-FLOAT", "ACL2-USER", "COMMON-LISP"),
("MAKE-STRING-INPUT-STREAM", "ACL2-USER", "COMMON-LISP"),
("MOST-POSITIVE-SHORT-FLOAT", "ACL2-USER", "COMMON-LISP"),
("MAKE-STRING-OUTPUT-STREAM", "ACL2-USER", "COMMON-LISP"),
("MOST-POSITIVE-SINGLE-FLOAT", "ACL2-USER", "COMMON-LISP"),
("MAKE-SYMBOL", "ACL2-USER", "COMMON-LISP"),
("MUFFLE-WARNING", "ACL2-USER", "COMMON-LISP"),
("MAKE-SYNONYM-STREAM", "ACL2-USER", "COMMON-LISP"),
("MULTIPLE-VALUE-BIND", "ACL2-USER", "COMMON-LISP"),
("MAKE-TWO-WAY-STREAM", "ACL2-USER", "COMMON-LISP"),
("MULTIPLE-VALUE-CALL", "ACL2-USER", "COMMON-LISP"),
("MAKUNBOUND", "ACL2-USER", "COMMON-LISP"),
("MULTIPLE-VALUE-LIST", "ACL2-USER", "COMMON-LISP"),
("MAP", "ACL2-USER", "COMMON-LISP"),
("MULTIPLE-VALUE-PROG1", "ACL2-USER", "COMMON-LISP"),
("MAP-INTO", "ACL2-USER", "COMMON-LISP"),
("MULTIPLE-VALUE-SETQ", "ACL2-USER", "COMMON-LISP"),
("MAPC", "ACL2-USER", "COMMON-LISP"),
("MULTIPLE-VALUES-LIMIT", "ACL2-USER", "COMMON-LISP"),
("MAPCAN", "ACL2-USER", "COMMON-LISP"),
("NAME-CHAR", "ACL2-USER", "COMMON-LISP"),
("MAPCAR", "ACL2-USER", "COMMON-LISP"),
("NAMESTRING", "ACL2-USER", "COMMON-LISP"),
("MAPCON", "ACL2-USER", "COMMON-LISP"),
("NBUTLAST", "ACL2-USER", "COMMON-LISP"),
("MAPHASH", "ACL2-USER", "COMMON-LISP"),
("NCONC", "ACL2-USER", "COMMON-LISP"),
("MAPL", "ACL2-USER", "COMMON-LISP"),
("NEXT-METHOD-P", "ACL2-USER", "COMMON-LISP"),
("MAPLIST", "ACL2-USER", "COMMON-LISP"),
("NIL", "ACL2-USER", "COMMON-LISP"),
("NINTERSECTION", "ACL2-USER", "COMMON-LISP"),
("PACKAGE-ERROR", "ACL2-USER", "COMMON-LISP"),
("NINTH", "ACL2-USER", "COMMON-LISP"),
("PACKAGE-ERROR-PACKAGE", "ACL2-USER", "COMMON-LISP"),
("NO-APPLICABLE-METHOD", "ACL2-USER", "COMMON-LISP"),
("PACKAGE-NAME", "ACL2-USER", "COMMON-LISP"),
("NO-NEXT-METHOD", "ACL2-USER", "COMMON-LISP"),
("PACKAGE-NICKNAMES", "ACL2-USER", "COMMON-LISP"),
("NOT", "ACL2-USER", "COMMON-LISP"),
("PACKAGE-SHADOWING-SYMBOLS", "ACL2-USER", "COMMON-LISP"),
("NOTANY", "ACL2-USER", "COMMON-LISP"),
("PACKAGE-USE-LIST", "ACL2-USER", "COMMON-LISP"),
("NOTEVERY", "ACL2-USER", "COMMON-LISP"),
("PACKAGE-USED-BY-LIST", "ACL2-USER", "COMMON-LISP"),
("NOTINLINE", "ACL2-USER", "COMMON-LISP"),
("PACKAGEP", "ACL2-USER", "COMMON-LISP"),
("NRECONC", "ACL2-USER", "COMMON-LISP"),
("PAIRLIS", "ACL2-USER", "COMMON-LISP"),
("NREVERSE", "ACL2-USER", "COMMON-LISP"),
("PARSE-ERROR", "ACL2-USER", "COMMON-LISP"),
("NSET-DIFFERENCE", "ACL2-USER", "COMMON-LISP"),
("PARSE-INTEGER", "ACL2-USER", "COMMON-LISP"),
("NSET-EXCLUSIVE-OR", "ACL2-USER", "COMMON-LISP"),
("PARSE-NAMESTRING", "ACL2-USER", "COMMON-LISP"),
("NSTRING-CAPITALIZE", "ACL2-USER", "COMMON-LISP"),
("PATHNAME", "ACL2-USER", "COMMON-LISP"),
("NSTRING-DOWNCASE", "ACL2-USER", "COMMON-LISP"),
("PATHNAME-DEVICE", "ACL2-USER", "COMMON-LISP"),
("NSTRING-UPCASE", "ACL2-USER", "COMMON-LISP"),
("PATHNAME-DIRECTORY", "ACL2-USER", "COMMON-LISP"),
("NSUBLIS", "ACL2-USER", "COMMON-LISP"),
("PATHNAME-HOST", "ACL2-USER", "COMMON-LISP"),
("NSUBST", "ACL2-USER", "COMMON-LISP"),
("PATHNAME-MATCH-P", "ACL2-USER", "COMMON-LISP"),
("NSUBST-IF", "ACL2-USER", "COMMON-LISP"),
("PATHNAME-NAME", "ACL2-USER", "COMMON-LISP"),
("NSUBST-IF-NOT", "ACL2-USER", "COMMON-LISP"),
("PATHNAME-TYPE", "ACL2-USER", "COMMON-LISP"),
("NSUBSTITUTE", "ACL2-USER", "COMMON-LISP"),
("PATHNAME-VERSION", "ACL2-USER", "COMMON-LISP"),
("NSUBSTITUTE-IF", "ACL2-USER", "COMMON-LISP"),
("PATHNAMEP", "ACL2-USER", "COMMON-LISP"),
("NSUBSTITUTE-IF-NOT", "ACL2-USER", "COMMON-LISP"),
("PEEK-CHAR", "ACL2-USER", "COMMON-LISP"),
("NTH", "ACL2-USER", "COMMON-LISP"),
("PHASE", "ACL2-USER", "COMMON-LISP"),
("NTH-VALUE", "ACL2-USER", "COMMON-LISP"),
("PI", "ACL2-USER", "COMMON-LISP"),
("NTHCDR", "ACL2-USER", "COMMON-LISP"),
("PLUSP", "ACL2-USER", "COMMON-LISP"),
("NULL", "ACL2-USER", "COMMON-LISP"),
("POP", "ACL2-USER", "COMMON-LISP"),
("NUMBER", "ACL2-USER", "COMMON-LISP"),
("POSITION", "ACL2-USER", "COMMON-LISP"),
("NUMBERP", "ACL2-USER", "COMMON-LISP"),
("POSITION-IF", "ACL2-USER", "COMMON-LISP"),
("NUMERATOR", "ACL2-USER", "COMMON-LISP"),
("POSITION-IF-NOT", "ACL2-USER", "COMMON-LISP"),
("NUNION", "ACL2-USER", "COMMON-LISP"),
("PPRINT", "ACL2-USER", "COMMON-LISP"),
("ODDP", "ACL2-USER", "COMMON-LISP"),
("PPRINT-DISPATCH", "ACL2-USER", "COMMON-LISP"),
("OPEN", "ACL2-USER", "COMMON-LISP"),
("PPRINT-EXIT-IF-LIST-EXHAUSTED", "ACL2-USER", "COMMON-LISP"),
("OPEN-STREAM-P", "ACL2-USER", "COMMON-LISP"),
("PPRINT-FILL", "ACL2-USER", "COMMON-LISP"),
("OPTIMIZE", "ACL2-USER", "COMMON-LISP"),
("PPRINT-INDENT", "ACL2-USER", "COMMON-LISP"),
("OR", "ACL2-USER", "COMMON-LISP"),
("PPRINT-LINEAR", "ACL2-USER", "COMMON-LISP"),
("OTHERWISE", "ACL2-USER", "COMMON-LISP"),
("PPRINT-LOGICAL-BLOCK", "ACL2-USER", "COMMON-LISP"),
("OUTPUT-STREAM-P", "ACL2-USER", "COMMON-LISP"),
("PPRINT-NEWLINE", "ACL2-USER", "COMMON-LISP"),
("PACKAGE", "ACL2-USER", "COMMON-LISP"),
("PPRINT-POP", "ACL2-USER", "COMMON-LISP"),
("PPRINT-TAB", "ACL2-USER", "COMMON-LISP"),
("READ-CHAR", "ACL2-USER", "COMMON-LISP"),
("PPRINT-TABULAR", "ACL2-USER", "COMMON-LISP"),
("READ-CHAR-NO-HANG", "ACL2-USER", "COMMON-LISP"),
("PRIN1", "ACL2-USER", "COMMON-LISP"),
("READ-DELIMITED-LIST", "ACL2-USER", "COMMON-LISP"),
("PRIN1-TO-STRING", "ACL2-USER", "COMMON-LISP"),
("READ-FROM-STRING", "ACL2-USER", "COMMON-LISP"),
("PRINC", "ACL2-USER", "COMMON-LISP"),
("READ-LINE", "ACL2-USER", "COMMON-LISP"),
("PRINC-TO-STRING", "ACL2-USER", "COMMON-LISP"),
("READ-PRESERVING-WHITESPACE", "ACL2-USER", "COMMON-LISP"),
("PRINT", "ACL2-USER", "COMMON-LISP"),
("READ-SEQUENCE", "ACL2-USER", "COMMON-LISP"),
("PRINT-NOT-READABLE", "ACL2-USER", "COMMON-LISP"),
("READER-ERROR", "ACL2-USER", "COMMON-LISP"),
("PRINT-NOT-READABLE-OBJECT", "ACL2-USER", "COMMON-LISP"),
("READTABLE", "ACL2-USER", "COMMON-LISP"),
("PRINT-OBJECT", "ACL2-USER", "COMMON-LISP"),
("READTABLE-CASE", "ACL2-USER", "COMMON-LISP"),
("PRINT-UNREADABLE-OBJECT", "ACL2-USER", "COMMON-LISP"),
("READTABLEP", "ACL2-USER", "COMMON-LISP"),
("PROBE-FILE", "ACL2-USER", "COMMON-LISP"),
("REAL", "ACL2-USER", "COMMON-LISP"),
("PROCLAIM", "ACL2-USER", "COMMON-LISP"),
("REALP", "ACL2-USER", "COMMON-LISP"),
("PROG", "ACL2-USER", "COMMON-LISP"),
("REALPART", "ACL2-USER", "COMMON-LISP"),
("PROG*", "ACL2-USER", "COMMON-LISP"),
("REDUCE", "ACL2-USER", "COMMON-LISP"),
("PROG1", "ACL2-USER", "COMMON-LISP"),
("REINITIALIZE-INSTANCE", "ACL2-USER", "COMMON-LISP"),
("PROG2", "ACL2-USER", "COMMON-LISP"),
("REM", "ACL2-USER", "COMMON-LISP"),
("PROGN", "ACL2-USER", "COMMON-LISP"),
("REMF", "ACL2-USER", "COMMON-LISP"),
("PROGRAM-ERROR", "ACL2-USER", "COMMON-LISP"),
("REMHASH", "ACL2-USER", "COMMON-LISP"),
("PROGV", "ACL2-USER", "COMMON-LISP"),
("REMOVE", "ACL2-USER", "COMMON-LISP"),
("PROVIDE", "ACL2-USER", "COMMON-LISP"),
("REMOVE-DUPLICATES", "ACL2-USER", "COMMON-LISP"),
("PSETF", "ACL2-USER", "COMMON-LISP"),
("REMOVE-IF", "ACL2-USER", "COMMON-LISP"),
("PSETQ", "ACL2-USER", "COMMON-LISP"),
("REMOVE-IF-NOT", "ACL2-USER", "COMMON-LISP"),
("PUSH", "ACL2-USER", "COMMON-LISP"),
("REMOVE-METHOD", "ACL2-USER", "COMMON-LISP"),
("PUSHNEW", "ACL2-USER", "COMMON-LISP"),
("REMPROP", "ACL2-USER", "COMMON-LISP"),
("QUOTE", "ACL2-USER", "COMMON-LISP"),
("RENAME-FILE", "ACL2-USER", "COMMON-LISP"),
("RANDOM", "ACL2-USER", "COMMON-LISP"),
("RENAME-PACKAGE", "ACL2-USER", "COMMON-LISP"),
("RANDOM-STATE", "ACL2-USER", "COMMON-LISP"),
("REPLACE", "ACL2-USER", "COMMON-LISP"),
("RANDOM-STATE-P", "ACL2-USER", "COMMON-LISP"),
("REQUIRE", "ACL2-USER", "COMMON-LISP"),
("RASSOC", "ACL2-USER", "COMMON-LISP"),
("REST", "ACL2-USER", "COMMON-LISP"),
("RASSOC-IF", "ACL2-USER", "COMMON-LISP"),
("RESTART", "ACL2-USER", "COMMON-LISP"),
("RASSOC-IF-NOT", "ACL2-USER", "COMMON-LISP"),
("RESTART-BIND", "ACL2-USER", "COMMON-LISP"),
("RATIO", "ACL2-USER", "COMMON-LISP"),
("RESTART-CASE", "ACL2-USER", "COMMON-LISP"),
("RATIONAL", "ACL2-USER", "COMMON-LISP"),
("RESTART-NAME", "ACL2-USER", "COMMON-LISP"),
("RATIONALIZE", "ACL2-USER", "COMMON-LISP"),
("RETURN", "ACL2-USER", "COMMON-LISP"),
("RATIONALP", "ACL2-USER", "COMMON-LISP"),
("RETURN-FROM", "ACL2-USER", "COMMON-LISP"),
("READ", "ACL2-USER", "COMMON-LISP"),
("REVAPPEND", "ACL2-USER", "COMMON-LISP"),
("READ-BYTE", "ACL2-USER", "COMMON-LISP"),
("REVERSE", "ACL2-USER", "COMMON-LISP"),
("ROOM", "ACL2-USER", "COMMON-LISP"),
("SIMPLE-BIT-VECTOR", "ACL2-USER", "COMMON-LISP"),
("ROTATEF", "ACL2-USER", "COMMON-LISP"),
("SIMPLE-BIT-VECTOR-P", "ACL2-USER", "COMMON-LISP"),
("ROUND", "ACL2-USER", "COMMON-LISP"),
("SIMPLE-CONDITION", "ACL2-USER", "COMMON-LISP"),
("ROW-MAJOR-AREF", "ACL2-USER", "COMMON-LISP"),
("SIMPLE-CONDITION-FORMAT-ARGUMENTS", "ACL2-USER", "COMMON-LISP"),
("RPLACA", "ACL2-USER", "COMMON-LISP"),
("SIMPLE-CONDITION-FORMAT-CONTROL", "ACL2-USER", "COMMON-LISP"),
("RPLACD", "ACL2-USER", "COMMON-LISP"),
("SIMPLE-ERROR", "ACL2-USER", "COMMON-LISP"),
("SAFETY", "ACL2-USER", "COMMON-LISP"),
("SIMPLE-STRING", "ACL2-USER", "COMMON-LISP"),
("SATISFIES", "ACL2-USER", "COMMON-LISP"),
("SIMPLE-STRING-P", "ACL2-USER", "COMMON-LISP"),
("SBIT", "ACL2-USER", "COMMON-LISP"),
("SIMPLE-TYPE-ERROR", "ACL2-USER", "COMMON-LISP"),
("SCALE-FLOAT", "ACL2-USER", "COMMON-LISP"),
("SIMPLE-VECTOR", "ACL2-USER", "COMMON-LISP"),
("SCHAR", "ACL2-USER", "COMMON-LISP"),
("SIMPLE-VECTOR-P", "ACL2-USER", "COMMON-LISP"),
("SEARCH", "ACL2-USER", "COMMON-LISP"),
("SIMPLE-WARNING", "ACL2-USER", "COMMON-LISP"),
("SECOND", "ACL2-USER", "COMMON-LISP"),
("SIN", "ACL2-USER", "COMMON-LISP"),
("SEQUENCE", "ACL2-USER", "COMMON-LISP"),
("SINGLE-FLOAT", "ACL2-USER", "COMMON-LISP"),
("SERIOUS-CONDITION", "ACL2-USER", "COMMON-LISP"),
("SINGLE-FLOAT-EPSILON", "ACL2-USER", "COMMON-LISP"),
("SET", "ACL2-USER", "COMMON-LISP"),
("SINGLE-FLOAT-NEGATIVE-EPSILON", "ACL2-USER", "COMMON-LISP"),
("SET-DIFFERENCE", "ACL2-USER", "COMMON-LISP"),
("SINH", "ACL2-USER", "COMMON-LISP"),
("SET-DISPATCH-MACRO-CHARACTER", "ACL2-USER", "COMMON-LISP"),
("SIXTH", "ACL2-USER", "COMMON-LISP"),
("SET-EXCLUSIVE-OR", "ACL2-USER", "COMMON-LISP"),
("SLEEP", "ACL2-USER", "COMMON-LISP"),
("SET-MACRO-CHARACTER", "ACL2-USER", "COMMON-LISP"),
("SLOT-BOUNDP", "ACL2-USER", "COMMON-LISP"),
("SET-PPRINT-DISPATCH", "ACL2-USER", "COMMON-LISP"),
("SLOT-EXISTS-P", "ACL2-USER", "COMMON-LISP"),
("SET-SYNTAX-FROM-CHAR", "ACL2-USER", "COMMON-LISP"),
("SLOT-MAKUNBOUND", "ACL2-USER", "COMMON-LISP"),
("SETF", "ACL2-USER", "COMMON-LISP"),
("SLOT-MISSING", "ACL2-USER", "COMMON-LISP"),
("SETQ", "ACL2-USER", "COMMON-LISP"),
("SLOT-UNBOUND", "ACL2-USER", "COMMON-LISP"),
("SEVENTH", "ACL2-USER", "COMMON-LISP"),
("SLOT-VALUE", "ACL2-USER", "COMMON-LISP"),
("SHADOW", "ACL2-USER", "COMMON-LISP"),
("SOFTWARE-TYPE", "ACL2-USER", "COMMON-LISP"),
("SHADOWING-IMPORT", "ACL2-USER", "COMMON-LISP"),
("SOFTWARE-VERSION", "ACL2-USER", "COMMON-LISP"),
("SHARED-INITIALIZE", "ACL2-USER", "COMMON-LISP"),
("SOME", "ACL2-USER", "COMMON-LISP"),
("SHIFTF", "ACL2-USER", "COMMON-LISP"),
("SORT", "ACL2-USER", "COMMON-LISP"),
("SHORT-FLOAT", "ACL2-USER", "COMMON-LISP"),
("SPACE", "ACL2-USER", "COMMON-LISP"),
("SHORT-FLOAT-EPSILON", "ACL2-USER", "COMMON-LISP"),
("SPECIAL", "ACL2-USER", "COMMON-LISP"),
("SHORT-FLOAT-NEGATIVE-EPSILON", "ACL2-USER", "COMMON-LISP"),
("SPECIAL-OPERATOR-P", "ACL2-USER", "COMMON-LISP"),
("SHORT-SITE-NAME", "ACL2-USER", "COMMON-LISP"),
("SPEED", "ACL2-USER", "COMMON-LISP"),
("SIGNAL", "ACL2-USER", "COMMON-LISP"),
("SQRT", "ACL2-USER", "COMMON-LISP"),
("SIGNED-BYTE", "ACL2-USER", "COMMON-LISP"),
("STABLE-SORT", "ACL2-USER", "COMMON-LISP"),
("SIGNUM", "ACL2-USER", "COMMON-LISP"),
("STANDARD", "ACL2-USER", "COMMON-LISP"),
("SIMPLE-ARRAY", "ACL2-USER", "COMMON-LISP"),
("STANDARD-CHAR", "ACL2-USER", "COMMON-LISP"),
("SIMPLE-BASE-STRING", "ACL2-USER", "COMMON-LISP"),
("STANDARD-CHAR-P", "ACL2-USER", "COMMON-LISP"),
("STANDARD-CLASS", "ACL2-USER", "COMMON-LISP"),
("SUBLIS", "ACL2-USER", "COMMON-LISP"),
("STANDARD-GENERIC-FUNCTION", "ACL2-USER", "COMMON-LISP"),
("SUBSEQ", "ACL2-USER", "COMMON-LISP"),
("STANDARD-METHOD", "ACL2-USER", "COMMON-LISP"),
("SUBSETP", "ACL2-USER", "COMMON-LISP"),
("STANDARD-OBJECT", "ACL2-USER", "COMMON-LISP"),
("SUBST", "ACL2-USER", "COMMON-LISP"),
("STEP", "ACL2-USER", "COMMON-LISP"),
("SUBST-IF", "ACL2-USER", "COMMON-LISP"),
("STORAGE-CONDITION", "ACL2-USER", "COMMON-LISP"),
("SUBST-IF-NOT", "ACL2-USER", "COMMON-LISP"),
("STORE-VALUE", "ACL2-USER", "COMMON-LISP"),
("SUBSTITUTE", "ACL2-USER", "COMMON-LISP"),
("STREAM", "ACL2-USER", "COMMON-LISP"),
("SUBSTITUTE-IF", "ACL2-USER", "COMMON-LISP"),
("STREAM-ELEMENT-TYPE", "ACL2-USER", "COMMON-LISP"),
("SUBSTITUTE-IF-NOT", "ACL2-USER", "COMMON-LISP"),
("STREAM-ERROR", "ACL2-USER", "COMMON-LISP"),
("SUBTYPEP", "ACL2-USER", "COMMON-LISP"),
("STREAM-ERROR-STREAM", "ACL2-USER", "COMMON-LISP"),
("SVREF", "ACL2-USER", "COMMON-LISP"),
("STREAM-EXTERNAL-FORMAT", "ACL2-USER", "COMMON-LISP"),
("SXHASH", "ACL2-USER", "COMMON-LISP"),
("STREAMP", "ACL2-USER", "COMMON-LISP"),
("SYMBOL", "ACL2-USER", "COMMON-LISP"),
("STRING", "ACL2-USER", "COMMON-LISP"),
("SYMBOL-FUNCTION", "ACL2-USER", "COMMON-LISP"),
("STRING-CAPITALIZE", "ACL2-USER", "COMMON-LISP"),
("SYMBOL-MACROLET", "ACL2-USER", "COMMON-LISP"),
("STRING-DOWNCASE", "ACL2-USER", "COMMON-LISP"),
("SYMBOL-NAME", "ACL2-USER", "COMMON-LISP"),
("STRING-EQUAL", "ACL2-USER", "COMMON-LISP"),
("SYMBOL-PACKAGE", "ACL2-USER", "COMMON-LISP"),
("STRING-GREATERP", "ACL2-USER", "COMMON-LISP"),
("SYMBOL-PLIST", "ACL2-USER", "COMMON-LISP"),
("STRING-LEFT-TRIM", "ACL2-USER", "COMMON-LISP"),
("SYMBOL-VALUE", "ACL2-USER", "COMMON-LISP"),
("STRING-LESSP", "ACL2-USER", "COMMON-LISP"),
("SYMBOLP", "ACL2-USER", "COMMON-LISP"),
("STRING-NOT-EQUAL", "ACL2-USER", "COMMON-LISP"),
("SYNONYM-STREAM", "ACL2-USER", "COMMON-LISP"),
("STRING-NOT-GREATERP", "ACL2-USER", "COMMON-LISP"),
("SYNONYM-STREAM-SYMBOL", "ACL2-USER", "COMMON-LISP"),
("STRING-NOT-LESSP", "ACL2-USER", "COMMON-LISP"),
("T", "ACL2-USER", "COMMON-LISP"),
("STRING-RIGHT-TRIM", "ACL2-USER", "COMMON-LISP"),
("TAGBODY", "ACL2-USER", "COMMON-LISP"),
("STRING-STREAM", "ACL2-USER", "COMMON-LISP"),
("TAILP", "ACL2-USER", "COMMON-LISP"),
("STRING-TRIM", "ACL2-USER", "COMMON-LISP"),
("TAN", "ACL2-USER", "COMMON-LISP"),
("STRING-UPCASE", "ACL2-USER", "COMMON-LISP"),
("TANH", "ACL2-USER", "COMMON-LISP"),
("STRING/=", "ACL2-USER", "COMMON-LISP"),
("TENTH", "ACL2-USER", "COMMON-LISP"),
("STRING<", "ACL2-USER", "COMMON-LISP"),
("TERPRI", "ACL2-USER", "COMMON-LISP"),
("STRING<=", "ACL2-USER", "COMMON-LISP"),
("THE", "ACL2-USER", "COMMON-LISP"),
("STRING=", "ACL2-USER", "COMMON-LISP"),
("THIRD", "ACL2-USER", "COMMON-LISP"),
("STRING>", "ACL2-USER", "COMMON-LISP"),
("THROW", "ACL2-USER", "COMMON-LISP"),
("STRING>=", "ACL2-USER", "COMMON-LISP"),
("TIME", "ACL2-USER", "COMMON-LISP"),
("STRINGP", "ACL2-USER", "COMMON-LISP"),
("TRACE", "ACL2-USER", "COMMON-LISP"),
("STRUCTURE", "ACL2-USER", "COMMON-LISP"),
("TRANSLATE-LOGICAL-PATHNAME", "ACL2-USER", "COMMON-LISP"),
("STRUCTURE-CLASS", "ACL2-USER", "COMMON-LISP"),
("TRANSLATE-PATHNAME", "ACL2-USER", "COMMON-LISP"),
("STRUCTURE-OBJECT", "ACL2-USER", "COMMON-LISP"),
("TREE-EQUAL", "ACL2-USER", "COMMON-LISP"),
("STYLE-WARNING", "ACL2-USER", "COMMON-LISP"),
("TRUENAME", "ACL2-USER", "COMMON-LISP"),
("TRUNCATE", "ACL2-USER", "COMMON-LISP"),
("VALUES-LIST", "ACL2-USER", "COMMON-LISP"),
("TWO-WAY-STREAM", "ACL2-USER", "COMMON-LISP"),
("VARIABLE", "ACL2-USER", "COMMON-LISP"),
("TWO-WAY-STREAM-INPUT-STREAM", "ACL2-USER", "COMMON-LISP"),
("VECTOR", "ACL2-USER", "COMMON-LISP"),
("TWO-WAY-STREAM-OUTPUT-STREAM", "ACL2-USER", "COMMON-LISP"),
("VECTOR-POP", "ACL2-USER", "COMMON-LISP"),
("TYPE", "ACL2-USER", "COMMON-LISP"),
("VECTOR-PUSH", "ACL2-USER", "COMMON-LISP"),
("TYPE-ERROR", "ACL2-USER", "COMMON-LISP"),
("VECTOR-PUSH-EXTEND", "ACL2-USER", "COMMON-LISP"),
("TYPE-ERROR-DATUM", "ACL2-USER", "COMMON-LISP"),
("VECTORP", "ACL2-USER", "COMMON-LISP"),
("TYPE-ERROR-EXPECTED-TYPE", "ACL2-USER", "COMMON-LISP"),
("WARN", "ACL2-USER", "COMMON-LISP"),
("TYPE-OF", "ACL2-USER", "COMMON-LISP"),
("WARNING", "ACL2-USER", "COMMON-LISP"),
("TYPECASE", "ACL2-USER", "COMMON-LISP"),
("WHEN", "ACL2-USER", "COMMON-LISP"),
("TYPEP", "ACL2-USER", "COMMON-LISP"),
("WILD-PATHNAME-P", "ACL2-USER", "COMMON-LISP"),
("UNBOUND-SLOT", "ACL2-USER", "COMMON-LISP"),
("WITH-ACCESSORS", "ACL2-USER", "COMMON-LISP"),
("UNBOUND-SLOT-INSTANCE", "ACL2-USER", "COMMON-LISP"),
("WITH-COMPILATION-UNIT", "ACL2-USER", "COMMON-LISP"),
("UNBOUND-VARIABLE", "ACL2-USER", "COMMON-LISP"),
("WITH-CONDITION-RESTARTS", "ACL2-USER", "COMMON-LISP"),
("UNDEFINED-FUNCTION", "ACL2-USER", "COMMON-LISP"),
("WITH-HASH-TABLE-ITERATOR", "ACL2-USER", "COMMON-LISP"),
("UNEXPORT", "ACL2-USER", "COMMON-LISP"),
("WITH-INPUT-FROM-STRING", "ACL2-USER", "COMMON-LISP"),
("UNINTERN", "ACL2-USER", "COMMON-LISP"),
("WITH-OPEN-FILE", "ACL2-USER", "COMMON-LISP"),
("UNION", "ACL2-USER", "COMMON-LISP"),
("WITH-OPEN-STREAM", "ACL2-USER", "COMMON-LISP"),
("UNLESS", "ACL2-USER", "COMMON-LISP"),
("WITH-OUTPUT-TO-STRING", "ACL2-USER", "COMMON-LISP"),
("UNREAD-CHAR", "ACL2-USER", "COMMON-LISP"),
("WITH-PACKAGE-ITERATOR", "ACL2-USER", "COMMON-LISP"),
("UNSIGNED-BYTE", "ACL2-USER", "COMMON-LISP"),
("WITH-SIMPLE-RESTART", "ACL2-USER", "COMMON-LISP"),
("UNTRACE", "ACL2-USER", "COMMON-LISP"),
("WITH-SLOTS", "ACL2-USER", "COMMON-LISP"),
("UNUSE-PACKAGE", "ACL2-USER", "COMMON-LISP"),
("WITH-STANDARD-IO-SYNTAX", "ACL2-USER", "COMMON-LISP"),
("UNWIND-PROTECT", "ACL2-USER", "COMMON-LISP"),
("WRITE", "ACL2-USER", "COMMON-LISP"),
("UPDATE-INSTANCE-FOR-DIFFERENT-CLASS", "ACL2-USER", "COMMON-LISP"),
("WRITE-BYTE", "ACL2-USER", "COMMON-LISP"),
("UPDATE-INSTANCE-FOR-REDEFINED-CLASS", "ACL2-USER", "COMMON-LISP"),
("WRITE-CHAR", "ACL2-USER", "COMMON-LISP"),
("UPGRADED-ARRAY-ELEMENT-TYPE", "ACL2-USER", "COMMON-LISP"),
("WRITE-LINE", "ACL2-USER", "COMMON-LISP"),
("UPGRADED-COMPLEX-PART-TYPE", "ACL2-USER", "COMMON-LISP"),
("WRITE-SEQUENCE", "ACL2-USER", "COMMON-LISP"),
("UPPER-CASE-P", "ACL2-USER", "COMMON-LISP"),
("WRITE-STRING", "ACL2-USER", "COMMON-LISP"),
("USE-PACKAGE", "ACL2-USER", "COMMON-LISP"),
("WRITE-TO-STRING", "ACL2-USER", "COMMON-LISP"),
("USE-VALUE", "ACL2-USER", "COMMON-LISP"),
("Y-OR-N-P", "ACL2-USER", "COMMON-LISP"),
("USER-HOMEDIR-PATHNAME", "ACL2-USER", "COMMON-LISP"),
("YES-OR-NO-P", "ACL2-USER", "COMMON-LISP"),
("VALUES", "ACL2-USER", "COMMON-LISP"),
("ZEROP", "ACL2-USER", "COMMON-LISP"),
("&ALLOW-OTHER-KEYS", "ACL2", "COMMON-LISP"),
("*PRINT-MISER-WIDTH*", "ACL2", "COMMON-LISP"),
("&AUX", "ACL2", "COMMON-LISP"),
("*PRINT-PPRINT-DISPATCH*", "ACL2", "COMMON-LISP"),
("&BODY", "ACL2", "COMMON-LISP"),
("*PRINT-PRETTY*", "ACL2", "COMMON-LISP"),
("&ENVIRONMENT", "ACL2", "COMMON-LISP"),
("*PRINT-RADIX*", "ACL2", "COMMON-LISP"),
("&KEY", "ACL2", "COMMON-LISP"),
("*PRINT-READABLY*", "ACL2", "COMMON-LISP"),
("&OPTIONAL", "ACL2", "COMMON-LISP"),
("*PRINT-RIGHT-MARGIN*", "ACL2", "COMMON-LISP"),
("&REST", "ACL2", "COMMON-LISP"),
("*QUERY-IO*", "ACL2", "COMMON-LISP"),
("&WHOLE", "ACL2", "COMMON-LISP"),
("*RANDOM-STATE*", "ACL2", "COMMON-LISP"),
("*", "ACL2", "COMMON-LISP"),
("*READ-BASE*", "ACL2", "COMMON-LISP"),
("**", "ACL2", "COMMON-LISP"),
("*READ-DEFAULT-FLOAT-FORMAT*", "ACL2", "COMMON-LISP"),
("***", "ACL2", "COMMON-LISP"),
("*READ-EVAL*", "ACL2", "COMMON-LISP"),
("*BREAK-ON-SIGNALS*", "ACL2", "COMMON-LISP"),
("*READ-SUPPRESS*", "ACL2", "COMMON-LISP"),
("*COMPILE-FILE-PATHNAME*", "ACL2", "COMMON-LISP"),
("*READTABLE*", "ACL2", "COMMON-LISP"),
("*COMPILE-FILE-TRUENAME*", "ACL2", "COMMON-LISP"),
("*STANDARD-INPUT*", "ACL2", "COMMON-LISP"),
("*COMPILE-PRINT*", "ACL2", "COMMON-LISP"),
("*STANDARD-OUTPUT*", "ACL2", "COMMON-LISP"),
("*COMPILE-VERBOSE*", "ACL2", "COMMON-LISP"),
("*TERMINAL-IO*", "ACL2", "COMMON-LISP"),
("*DEBUG-IO*", "ACL2", "COMMON-LISP"),
("*TRACE-OUTPUT*", "ACL2", "COMMON-LISP"),
("*DEBUGGER-HOOK*", "ACL2", "COMMON-LISP"),
("+", "ACL2", "COMMON-LISP"),
("*DEFAULT-PATHNAME-DEFAULTS*", "ACL2", "COMMON-LISP"),
("++", "ACL2", "COMMON-LISP"),
("*ERROR-OUTPUT*", "ACL2", "COMMON-LISP"),
("+++", "ACL2", "COMMON-LISP"),
("*FEATURES*", "ACL2", "COMMON-LISP"),
("-", "ACL2", "COMMON-LISP"),
("*GENSYM-COUNTER*", "ACL2", "COMMON-LISP"),
("/", "ACL2", "COMMON-LISP"),
("*LOAD-PATHNAME*", "ACL2", "COMMON-LISP"),
("//", "ACL2", "COMMON-LISP"),
("*LOAD-PRINT*", "ACL2", "COMMON-LISP"),
("///", "ACL2", "COMMON-LISP"),
("*LOAD-TRUENAME*", "ACL2", "COMMON-LISP"),
("/=", "ACL2", "COMMON-LISP"),
("*LOAD-VERBOSE*", "ACL2", "COMMON-LISP"),
("1+", "ACL2", "COMMON-LISP"),
("*MACROEXPAND-HOOK*", "ACL2", "COMMON-LISP"),
("1-", "ACL2", "COMMON-LISP"),
("*MODULES*", "ACL2", "COMMON-LISP"),
("<", "ACL2", "COMMON-LISP"),
("*PACKAGE*", "ACL2", "COMMON-LISP"),
("<=", "ACL2", "COMMON-LISP"),
("*PRINT-ARRAY*", "ACL2", "COMMON-LISP"),
("=", "ACL2", "COMMON-LISP"),
("*PRINT-BASE*", "ACL2", "COMMON-LISP"),
(">", "ACL2", "COMMON-LISP"),
("*PRINT-CASE*", "ACL2", "COMMON-LISP"),
(">=", "ACL2", "COMMON-LISP"),
("*PRINT-CIRCLE*", "ACL2", "COMMON-LISP"),
("ABORT", "ACL2", "COMMON-LISP"),
("*PRINT-ESCAPE*", "ACL2", "COMMON-LISP"),
("ABS", "ACL2", "COMMON-LISP"),
("*PRINT-GENSYM*", "ACL2", "COMMON-LISP"),
("ACONS", "ACL2", "COMMON-LISP"),
("*PRINT-LENGTH*", "ACL2", "COMMON-LISP"),
("ACOS", "ACL2", "COMMON-LISP"),
("*PRINT-LEVEL*", "ACL2", "COMMON-LISP"),
("ACOSH", "ACL2", "COMMON-LISP"),
("*PRINT-LINES*", "ACL2", "COMMON-LISP"),
("ADD-METHOD", "ACL2", "COMMON-LISP"),
("ADJOIN", "ACL2", "COMMON-LISP"),
("ATOM", "ACL2", "COMMON-LISP"),
("BOUNDP", "ACL2", "COMMON-LISP"),
("ADJUST-ARRAY", "ACL2", "COMMON-LISP"),
("BASE-CHAR", "ACL2", "COMMON-LISP"),
("BREAK", "ACL2", "COMMON-LISP"),
("ADJUSTABLE-ARRAY-P", "ACL2", "COMMON-LISP"),
("BASE-STRING", "ACL2", "COMMON-LISP"),
("BROADCAST-STREAM", "ACL2", "COMMON-LISP"),
("ALLOCATE-INSTANCE", "ACL2", "COMMON-LISP"),
("BIGNUM", "ACL2", "COMMON-LISP"),
("BROADCAST-STREAM-STREAMS", "ACL2", "COMMON-LISP"),
("ALPHA-CHAR-P", "ACL2", "COMMON-LISP"),
("BIT", "ACL2", "COMMON-LISP"),
("BUILT-IN-CLASS", "ACL2", "COMMON-LISP"),
("ALPHANUMERICP", "ACL2", "COMMON-LISP"),
("BIT-AND", "ACL2", "COMMON-LISP"),
("BUTLAST", "ACL2", "COMMON-LISP"),
("AND", "ACL2", "COMMON-LISP"),
("BIT-ANDC1", "ACL2", "COMMON-LISP"),
("BYTE", "ACL2", "COMMON-LISP"),
("APPEND", "ACL2", "COMMON-LISP"),
("BIT-ANDC2", "ACL2", "COMMON-LISP"),
("BYTE-POSITION", "ACL2", "COMMON-LISP"),
("APPLY", "ACL2", "COMMON-LISP"),
("BIT-EQV", "ACL2", "COMMON-LISP"),
("BYTE-SIZE", "ACL2", "COMMON-LISP"),
("APROPOS", "ACL2", "COMMON-LISP"),
("BIT-IOR", "ACL2", "COMMON-LISP"),
("CAAAAR", "ACL2", "COMMON-LISP"),
("APROPOS-LIST", "ACL2", "COMMON-LISP"),
("BIT-NAND", "ACL2", "COMMON-LISP"),
("CAAADR", "ACL2", "COMMON-LISP"),
("AREF", "ACL2", "COMMON-LISP"),
("BIT-NOR", "ACL2", "COMMON-LISP"),
("CAAAR", "ACL2", "COMMON-LISP"),
("ARITHMETIC-ERROR", "ACL2", "COMMON-LISP"),
("BIT-NOT", "ACL2", "COMMON-LISP"),
("CAADAR", "ACL2", "COMMON-LISP"),
("ARITHMETIC-ERROR-OPERANDS", "ACL2", "COMMON-LISP"),
("BIT-ORC1", "ACL2", "COMMON-LISP"),
("CAADDR", "ACL2", "COMMON-LISP"),
("ARITHMETIC-ERROR-OPERATION", "ACL2", "COMMON-LISP"),
("BIT-ORC2", "ACL2", "COMMON-LISP"),
("CAADR", "ACL2", "COMMON-LISP"),
("ARRAY", "ACL2", "COMMON-LISP"),
("BIT-VECTOR", "ACL2", "COMMON-LISP"),
("CAAR", "ACL2", "COMMON-LISP"),
("ARRAY-DIMENSION", "ACL2", "COMMON-LISP"),
("BIT-VECTOR-P", "ACL2", "COMMON-LISP"),
("CADAAR", "ACL2", "COMMON-LISP"),
("ARRAY-DIMENSION-LIMIT", "ACL2", "COMMON-LISP"),
("BIT-XOR", "ACL2", "COMMON-LISP"),
("CADADR", "ACL2", "COMMON-LISP"),
("ARRAY-DIMENSIONS", "ACL2", "COMMON-LISP"),
("BLOCK", "ACL2", "COMMON-LISP"),
("CADAR", "ACL2", "COMMON-LISP"),
("ARRAY-DISPLACEMENT", "ACL2", "COMMON-LISP"),
("BOOLE", "ACL2", "COMMON-LISP"),
("CADDAR", "ACL2", "COMMON-LISP"),
("ARRAY-ELEMENT-TYPE", "ACL2", "COMMON-LISP"),
("BOOLE-1", "ACL2", "COMMON-LISP"),
("CADDDR", "ACL2", "COMMON-LISP"),
("ARRAY-HAS-FILL-POINTER-P", "ACL2", "COMMON-LISP"),
("BOOLE-2", "ACL2", "COMMON-LISP"),
("CADDR", "ACL2", "COMMON-LISP"),
("ARRAY-IN-BOUNDS-P", "ACL2", "COMMON-LISP"),
("BOOLE-AND", "ACL2", "COMMON-LISP"),
("CADR", "ACL2", "COMMON-LISP"),
("ARRAY-RANK", "ACL2", "COMMON-LISP"),
("BOOLE-ANDC1", "ACL2", "COMMON-LISP"),
("CALL-ARGUMENTS-LIMIT", "ACL2", "COMMON-LISP"),
("ARRAY-RANK-LIMIT", "ACL2", "COMMON-LISP"),
("BOOLE-ANDC2", "ACL2", "COMMON-LISP"),
("CALL-METHOD", "ACL2", "COMMON-LISP"),
("ARRAY-ROW-MAJOR-INDEX", "ACL2", "COMMON-LISP"),
("BOOLE-C1", "ACL2", "COMMON-LISP"),
("CALL-NEXT-METHOD", "ACL2", "COMMON-LISP"),
("ARRAY-TOTAL-SIZE", "ACL2", "COMMON-LISP"),
("BOOLE-C2", "ACL2", "COMMON-LISP"),
("CAR", "ACL2", "COMMON-LISP"),
("ARRAY-TOTAL-SIZE-LIMIT", "ACL2", "COMMON-LISP"),
("BOOLE-CLR", "ACL2", "COMMON-LISP"),
("CASE", "ACL2", "COMMON-LISP"),
("ARRAYP", "ACL2", "COMMON-LISP"),
("BOOLE-EQV", "ACL2", "COMMON-LISP"),
("CATCH", "ACL2", "COMMON-LISP"),
("ASH", "ACL2", "COMMON-LISP"),
("BOOLE-IOR", "ACL2", "COMMON-LISP"),
("CCASE", "ACL2", "COMMON-LISP"),
("ASIN", "ACL2", "COMMON-LISP"),
("BOOLE-NAND", "ACL2", "COMMON-LISP"),
("CDAAAR", "ACL2", "COMMON-LISP"),
("ASINH", "ACL2", "COMMON-LISP"),
("BOOLE-NOR", "ACL2", "COMMON-LISP"),
("CDAADR", "ACL2", "COMMON-LISP"),
("ASSERT", "ACL2", "COMMON-LISP"),
("BOOLE-ORC1", "ACL2", "COMMON-LISP"),
("CDAAR", "ACL2", "COMMON-LISP"),
("ASSOC", "ACL2", "COMMON-LISP"),
("BOOLE-ORC2", "ACL2", "COMMON-LISP"),
("CDADAR", "ACL2", "COMMON-LISP"),
("ASSOC-IF", "ACL2", "COMMON-LISP"),
("BOOLE-SET", "ACL2", "COMMON-LISP"),
("CDADDR", "ACL2", "COMMON-LISP"),
("ASSOC-IF-NOT", "ACL2", "COMMON-LISP"),
("BOOLE-XOR", "ACL2", "COMMON-LISP"),
("CDADR", "ACL2", "COMMON-LISP"),
("ATAN", "ACL2", "COMMON-LISP"),
("BOOLEAN", "ACL2", "COMMON-LISP"),
("CDAR", "ACL2", "COMMON-LISP"),
("ATANH", "ACL2", "COMMON-LISP"),
("BOTH-CASE-P", "ACL2", "COMMON-LISP"),
("CDDAAR", "ACL2", "COMMON-LISP"),
("CDDADR", "ACL2", "COMMON-LISP"),
("CLEAR-INPUT", "ACL2", "COMMON-LISP"),
("COPY-TREE", "ACL2", "COMMON-LISP"),
("CDDAR", "ACL2", "COMMON-LISP"),
("CLEAR-OUTPUT", "ACL2", "COMMON-LISP"),
("COS", "ACL2", "COMMON-LISP"),
("CDDDAR", "ACL2", "COMMON-LISP"),
("CLOSE", "ACL2", "COMMON-LISP"),
("COSH", "ACL2", "COMMON-LISP"),
("CDDDDR", "ACL2", "COMMON-LISP"),
("CLRHASH", "ACL2", "COMMON-LISP"),
("COUNT", "ACL2", "COMMON-LISP"),
("CDDDR", "ACL2", "COMMON-LISP"),
("CODE-CHAR", "ACL2", "COMMON-LISP"),
("COUNT-IF", "ACL2", "COMMON-LISP"),
("CDDR", "ACL2", "COMMON-LISP"),
("COERCE", "ACL2", "COMMON-LISP"),
("COUNT-IF-NOT", "ACL2", "COMMON-LISP"),
("CDR", "ACL2", "COMMON-LISP"),
("COMPILATION-SPEED", "ACL2", "COMMON-LISP"),
("CTYPECASE", "ACL2", "COMMON-LISP"),
("CEILING", "ACL2", "COMMON-LISP"),
("COMPILE", "ACL2", "COMMON-LISP"),
("DEBUG", "ACL2", "COMMON-LISP"),
("CELL-ERROR", "ACL2", "COMMON-LISP"),
("COMPILE-FILE", "ACL2", "COMMON-LISP"),
("DECF", "ACL2", "COMMON-LISP"),
("CELL-ERROR-NAME", "ACL2", "COMMON-LISP"),
("COMPILE-FILE-PATHNAME", "ACL2", "COMMON-LISP"),
("DECLAIM", "ACL2", "COMMON-LISP"),
("CERROR", "ACL2", "COMMON-LISP"),
("COMPILED-FUNCTION", "ACL2", "COMMON-LISP"),
("DECLARATION", "ACL2", "COMMON-LISP"),
("CHANGE-CLASS", "ACL2", "COMMON-LISP"),
("COMPILED-FUNCTION-P", "ACL2", "COMMON-LISP"),
("DECLARE", "ACL2", "COMMON-LISP"),
("CHAR", "ACL2", "COMMON-LISP"),
("COMPILER-MACRO", "ACL2", "COMMON-LISP"),
("DECODE-FLOAT", "ACL2", "COMMON-LISP"),
("CHAR-CODE", "ACL2", "COMMON-LISP"),
("COMPILER-MACRO-FUNCTION", "ACL2", "COMMON-LISP"),
("DECODE-UNIVERSAL-TIME", "ACL2", "COMMON-LISP"),
("CHAR-CODE-LIMIT", "ACL2", "COMMON-LISP"),
("COMPLEMENT", "ACL2", "COMMON-LISP"),
("DEFCLASS", "ACL2", "COMMON-LISP"),
("CHAR-DOWNCASE", "ACL2", "COMMON-LISP"),
("COMPLEX", "ACL2", "COMMON-LISP"),
("DEFCONSTANT", "ACL2", "COMMON-LISP"),
("CHAR-EQUAL", "ACL2", "COMMON-LISP"),
("COMPLEXP", "ACL2", "COMMON-LISP"),
("DEFGENERIC", "ACL2", "COMMON-LISP"),
("CHAR-GREATERP", "ACL2", "COMMON-LISP"),
("COMPUTE-APPLICABLE-METHODS", "ACL2", "COMMON-LISP"),
("DEFINE-COMPILER-MACRO", "ACL2", "COMMON-LISP"),
("CHAR-INT", "ACL2", "COMMON-LISP"),
("COMPUTE-RESTARTS", "ACL2", "COMMON-LISP"),
("DEFINE-CONDITION", "ACL2", "COMMON-LISP"),
("CHAR-LESSP", "ACL2", "COMMON-LISP"),
("CONCATENATE", "ACL2", "COMMON-LISP"),
("DEFINE-METHOD-COMBINATION", "ACL2", "COMMON-LISP"),
("CHAR-NAME", "ACL2", "COMMON-LISP"),
("CONCATENATED-STREAM", "ACL2", "COMMON-LISP"),
("DEFINE-MODIFY-MACRO", "ACL2", "COMMON-LISP"),
("CHAR-NOT-EQUAL", "ACL2", "COMMON-LISP"),
("CONCATENATED-STREAM-STREAMS", "ACL2", "COMMON-LISP"),
("DEFINE-SETF-EXPANDER", "ACL2", "COMMON-LISP"),
("CHAR-NOT-GREATERP", "ACL2", "COMMON-LISP"),
("COND", "ACL2", "COMMON-LISP"),
("DEFINE-SYMBOL-MACRO", "ACL2", "COMMON-LISP"),
("CHAR-NOT-LESSP", "ACL2", "COMMON-LISP"),
("CONDITION", "ACL2", "COMMON-LISP"),
("DEFMACRO", "ACL2", "COMMON-LISP"),
("CHAR-UPCASE", "ACL2", "COMMON-LISP"),
("CONJUGATE", "ACL2", "COMMON-LISP"),
("DEFMETHOD", "ACL2", "COMMON-LISP"),
("CHAR/=", "ACL2", "COMMON-LISP"),
("CONS", "ACL2", "COMMON-LISP"),
("DEFPACKAGE", "ACL2", "COMMON-LISP"),
("CHAR<", "ACL2", "COMMON-LISP"),
("CONSP", "ACL2", "COMMON-LISP"),
("DEFPARAMETER", "ACL2", "COMMON-LISP"),
("CHAR<=", "ACL2", "COMMON-LISP"),
("CONSTANTLY", "ACL2", "COMMON-LISP"),
("DEFSETF", "ACL2", "COMMON-LISP"),
("CHAR=", "ACL2", "COMMON-LISP"),
("CONSTANTP", "ACL2", "COMMON-LISP"),
("DEFSTRUCT", "ACL2", "COMMON-LISP"),
("CHAR>", "ACL2", "COMMON-LISP"),
("CONTINUE", "ACL2", "COMMON-LISP"),
("DEFTYPE", "ACL2", "COMMON-LISP"),
("CHAR>=", "ACL2", "COMMON-LISP"),
("CONTROL-ERROR", "ACL2", "COMMON-LISP"),
("DEFUN", "ACL2", "COMMON-LISP"),
("CHARACTER", "ACL2", "COMMON-LISP"),
("COPY-ALIST", "ACL2", "COMMON-LISP"),
("DEFVAR", "ACL2", "COMMON-LISP"),
("CHARACTERP", "ACL2", "COMMON-LISP"),
("COPY-LIST", "ACL2", "COMMON-LISP"),
("DELETE", "ACL2", "COMMON-LISP"),
("CHECK-TYPE", "ACL2", "COMMON-LISP"),
("COPY-PPRINT-DISPATCH", "ACL2", "COMMON-LISP"),
("DELETE-DUPLICATES", "ACL2", "COMMON-LISP"),
("CIS", "ACL2", "COMMON-LISP"),
("COPY-READTABLE", "ACL2", "COMMON-LISP"),
("DELETE-FILE", "ACL2", "COMMON-LISP"),
("CLASS", "ACL2", "COMMON-LISP"),
("COPY-SEQ", "ACL2", "COMMON-LISP"),
("DELETE-IF", "ACL2", "COMMON-LISP"),
("CLASS-NAME", "ACL2", "COMMON-LISP"),
("COPY-STRUCTURE", "ACL2", "COMMON-LISP"),
("DELETE-IF-NOT", "ACL2", "COMMON-LISP"),
("CLASS-OF", "ACL2", "COMMON-LISP"),
("COPY-SYMBOL", "ACL2", "COMMON-LISP"),
("DELETE-PACKAGE", "ACL2", "COMMON-LISP"),
("DENOMINATOR", "ACL2", "COMMON-LISP"),
("EQ", "ACL2", "COMMON-LISP"),
("DEPOSIT-FIELD", "ACL2", "COMMON-LISP"),
("EQL", "ACL2", "COMMON-LISP"),
("DESCRIBE", "ACL2", "COMMON-LISP"),
("EQUAL", "ACL2", "COMMON-LISP"),
("DESCRIBE-OBJECT", "ACL2", "COMMON-LISP"),
("EQUALP", "ACL2", "COMMON-LISP"),
("DESTRUCTURING-BIND", "ACL2", "COMMON-LISP"),
("ERROR", "ACL2", "COMMON-LISP"),
("DIGIT-CHAR", "ACL2", "COMMON-LISP"),
("ETYPECASE", "ACL2", "COMMON-LISP"),
("DIGIT-CHAR-P", "ACL2", "COMMON-LISP"),
("EVAL", "ACL2", "COMMON-LISP"),
("DIRECTORY", "ACL2", "COMMON-LISP"),
("EVAL-WHEN", "ACL2", "COMMON-LISP"),
("DIRECTORY-NAMESTRING", "ACL2", "COMMON-LISP"),
("EVENP", "ACL2", "COMMON-LISP"),
("DISASSEMBLE", "ACL2", "COMMON-LISP"),
("EVERY", "ACL2", "COMMON-LISP"),
("DIVISION-BY-ZERO", "ACL2", "COMMON-LISP"),
("EXP", "ACL2", "COMMON-LISP"),
("DO", "ACL2", "COMMON-LISP"),
("EXPORT", "ACL2", "COMMON-LISP"),
("DO*", "ACL2", "COMMON-LISP"),
("EXPT", "ACL2", "COMMON-LISP"),
("DO-ALL-SYMBOLS", "ACL2", "COMMON-LISP"),
("EXTENDED-CHAR", "ACL2", "COMMON-LISP"),
("DO-EXTERNAL-SYMBOLS", "ACL2", "COMMON-LISP"),
("FBOUNDP", "ACL2", "COMMON-LISP"),
("DO-SYMBOLS", "ACL2", "COMMON-LISP"),
("FCEILING", "ACL2", "COMMON-LISP"),
("DOCUMENTATION", "ACL2", "COMMON-LISP"),
("FDEFINITION", "ACL2", "COMMON-LISP"),
("DOLIST", "ACL2", "COMMON-LISP"),
("FFLOOR", "ACL2", "COMMON-LISP"),
("DOTIMES", "ACL2", "COMMON-LISP"),
("FIFTH", "ACL2", "COMMON-LISP"),
("DOUBLE-FLOAT", "ACL2", "COMMON-LISP"),
("FILE-AUTHOR", "ACL2", "COMMON-LISP"),
("DOUBLE-FLOAT-EPSILON", "ACL2", "COMMON-LISP"),
("FILE-ERROR", "ACL2", "COMMON-LISP"),
("DOUBLE-FLOAT-NEGATIVE-EPSILON", "ACL2", "COMMON-LISP"),
("FILE-ERROR-PATHNAME", "ACL2", "COMMON-LISP"),
("DPB", "ACL2", "COMMON-LISP"),
("FILE-LENGTH", "ACL2", "COMMON-LISP"),
("DRIBBLE", "ACL2", "COMMON-LISP"),
("FILE-NAMESTRING", "ACL2", "COMMON-LISP"),
("DYNAMIC-EXTENT", "ACL2", "COMMON-LISP"),
("FILE-POSITION", "ACL2", "COMMON-LISP"),
("ECASE", "ACL2", "COMMON-LISP"),
("FILE-STREAM", "ACL2", "COMMON-LISP"),
("ECHO-STREAM", "ACL2", "COMMON-LISP"),
("FILE-STRING-LENGTH", "ACL2", "COMMON-LISP"),
("ECHO-STREAM-INPUT-STREAM", "ACL2", "COMMON-LISP"),
("FILE-WRITE-DATE", "ACL2", "COMMON-LISP"),
("ECHO-STREAM-OUTPUT-STREAM", "ACL2", "COMMON-LISP"),
("FILL", "ACL2", "COMMON-LISP"),
("ED", "ACL2", "COMMON-LISP"),
("FILL-POINTER", "ACL2", "COMMON-LISP"),
("EIGHTH", "ACL2", "COMMON-LISP"),
("FIND", "ACL2", "COMMON-LISP"),
("ELT", "ACL2", "COMMON-LISP"),
("FIND-ALL-SYMBOLS", "ACL2", "COMMON-LISP"),
("ENCODE-UNIVERSAL-TIME", "ACL2", "COMMON-LISP"),
("FIND-CLASS", "ACL2", "COMMON-LISP"),
("END-OF-FILE", "ACL2", "COMMON-LISP"),
("FIND-IF", "ACL2", "COMMON-LISP"),
("ENDP", "ACL2", "COMMON-LISP"),
("FIND-IF-NOT", "ACL2", "COMMON-LISP"),
("ENOUGH-NAMESTRING", "ACL2", "COMMON-LISP"),
("FIND-METHOD", "ACL2", "COMMON-LISP"),
("ENSURE-DIRECTORIES-EXIST", "ACL2", "COMMON-LISP"),
("FIND-PACKAGE", "ACL2", "COMMON-LISP"),
("ENSURE-GENERIC-FUNCTION", "ACL2", "COMMON-LISP"),
("FIND-RESTART", "ACL2", "COMMON-LISP"),
("FIND-SYMBOL", "ACL2", "COMMON-LISP"),
("GET-INTERNAL-RUN-TIME", "ACL2", "COMMON-LISP"),
("FINISH-OUTPUT", "ACL2", "COMMON-LISP"),
("GET-MACRO-CHARACTER", "ACL2", "COMMON-LISP"),
("FIRST", "ACL2", "COMMON-LISP"),
("GET-OUTPUT-STREAM-STRING", "ACL2", "COMMON-LISP"),
("FIXNUM", "ACL2", "COMMON-LISP"),
("GET-PROPERTIES", "ACL2", "COMMON-LISP"),
("FLET", "ACL2", "COMMON-LISP"),
("GET-SETF-EXPANSION", "ACL2", "COMMON-LISP"),
("FLOAT", "ACL2", "COMMON-LISP"),
("GET-UNIVERSAL-TIME", "ACL2", "COMMON-LISP"),
("FLOAT-DIGITS", "ACL2", "COMMON-LISP"),
("GETF", "ACL2", "COMMON-LISP"),
("FLOAT-PRECISION", "ACL2", "COMMON-LISP"),
("GETHASH", "ACL2", "COMMON-LISP"),
("FLOAT-RADIX", "ACL2", "COMMON-LISP"),
("GO", "ACL2", "COMMON-LISP"),
("FLOAT-SIGN", "ACL2", "COMMON-LISP"),
("GRAPHIC-CHAR-P", "ACL2", "COMMON-LISP"),
("FLOATING-POINT-INEXACT", "ACL2", "COMMON-LISP"),
("HANDLER-BIND", "ACL2", "COMMON-LISP"),
("FLOATING-POINT-INVALID-OPERATION", "ACL2", "COMMON-LISP"),
("HANDLER-CASE", "ACL2", "COMMON-LISP"),
("FLOATING-POINT-OVERFLOW", "ACL2", "COMMON-LISP"),
("HASH-TABLE", "ACL2", "COMMON-LISP"),
("FLOATING-POINT-UNDERFLOW", "ACL2", "COMMON-LISP"),
("HASH-TABLE-COUNT", "ACL2", "COMMON-LISP"),
("FLOATP", "ACL2", "COMMON-LISP"),
("HASH-TABLE-P", "ACL2", "COMMON-LISP"),
("FLOOR", "ACL2", "COMMON-LISP"),
("HASH-TABLE-REHASH-SIZE", "ACL2", "COMMON-LISP"),
("FMAKUNBOUND", "ACL2", "COMMON-LISP"),
("HASH-TABLE-REHASH-THRESHOLD", "ACL2", "COMMON-LISP"),
("FORCE-OUTPUT", "ACL2", "COMMON-LISP"),
("HASH-TABLE-SIZE", "ACL2", "COMMON-LISP"),
("FORMAT", "ACL2", "COMMON-LISP"),
("HASH-TABLE-TEST", "ACL2", "COMMON-LISP"),
("FORMATTER", "ACL2", "COMMON-LISP"),
("HOST-NAMESTRING", "ACL2", "COMMON-LISP"),
("FOURTH", "ACL2", "COMMON-LISP"),
("IDENTITY", "ACL2", "COMMON-LISP"),
("FRESH-LINE", "ACL2", "COMMON-LISP"),
("IF", "ACL2", "COMMON-LISP"),
("FROUND", "ACL2", "COMMON-LISP"),
("IGNORABLE", "ACL2", "COMMON-LISP"),
("FTRUNCATE", "ACL2", "COMMON-LISP"),
("IGNORE", "ACL2", "COMMON-LISP"),
("FTYPE", "ACL2", "COMMON-LISP"),
("IGNORE-ERRORS", "ACL2", "COMMON-LISP"),
("FUNCALL", "ACL2", "COMMON-LISP"),
("IMAGPART", "ACL2", "COMMON-LISP"),
("FUNCTION", "ACL2", "COMMON-LISP"),
("IMPORT", "ACL2", "COMMON-LISP"),
("FUNCTION-KEYWORDS", "ACL2", "COMMON-LISP"),
("IN-PACKAGE", "ACL2", "COMMON-LISP"),
("FUNCTION-LAMBDA-EXPRESSION", "ACL2", "COMMON-LISP"),
("INCF", "ACL2", "COMMON-LISP"),
("FUNCTIONP", "ACL2", "COMMON-LISP"),
("INITIALIZE-INSTANCE", "ACL2", "COMMON-LISP"),
("GCD", "ACL2", "COMMON-LISP"),
("INLINE", "ACL2", "COMMON-LISP"),
("GENERIC-FUNCTION", "ACL2", "COMMON-LISP"),
("INPUT-STREAM-P", "ACL2", "COMMON-LISP"),
("GENSYM", "ACL2", "COMMON-LISP"),
("INSPECT", "ACL2", "COMMON-LISP"),
("GENTEMP", "ACL2", "COMMON-LISP"),
("INTEGER", "ACL2", "COMMON-LISP"),
("GET", "ACL2", "COMMON-LISP"),
("INTEGER-DECODE-FLOAT", "ACL2", "COMMON-LISP"),
("GET-DECODED-TIME", "ACL2", "COMMON-LISP"),
("INTEGER-LENGTH", "ACL2", "COMMON-LISP"),
("GET-DISPATCH-MACRO-CHARACTER", "ACL2", "COMMON-LISP"),
("INTEGERP", "ACL2", "COMMON-LISP"),
("GET-INTERNAL-REAL-TIME", "ACL2", "COMMON-LISP"),
("INTERACTIVE-STREAM-P", "ACL2", "COMMON-LISP"),
("INTERN", "ACL2", "COMMON-LISP"),
("LISP-IMPLEMENTATION-TYPE", "ACL2", "COMMON-LISP"),
("INTERNAL-TIME-UNITS-PER-SECOND", "ACL2", "COMMON-LISP"),
("LISP-IMPLEMENTATION-VERSION", "ACL2", "COMMON-LISP"),
("INTERSECTION", "ACL2", "COMMON-LISP"),
("LIST", "ACL2", "COMMON-LISP"),
("INVALID-METHOD-ERROR", "ACL2", "COMMON-LISP"),
("LIST*", "ACL2", "COMMON-LISP"),
("INVOKE-DEBUGGER", "ACL2", "COMMON-LISP"),
("LIST-ALL-PACKAGES", "ACL2", "COMMON-LISP"),
("INVOKE-RESTART", "ACL2", "COMMON-LISP"),
("LIST-LENGTH", "ACL2", "COMMON-LISP"),
("INVOKE-RESTART-INTERACTIVELY", "ACL2", "COMMON-LISP"),
("LISTEN", "ACL2", "COMMON-LISP"),
("ISQRT", "ACL2", "COMMON-LISP"),
("LISTP", "ACL2", "COMMON-LISP"),
("KEYWORD", "ACL2", "COMMON-LISP"),
("LOAD", "ACL2", "COMMON-LISP"),
("KEYWORDP", "ACL2", "COMMON-LISP"),
("LOAD-LOGICAL-PATHNAME-TRANSLATIONS", "ACL2", "COMMON-LISP"),
("LABELS", "ACL2", "COMMON-LISP"),
("LOAD-TIME-VALUE", "ACL2", "COMMON-LISP"),
("LAMBDA", "ACL2", "COMMON-LISP"),
("LOCALLY", "ACL2", "COMMON-LISP"),
("LAMBDA-LIST-KEYWORDS", "ACL2", "COMMON-LISP"),
("LOG", "ACL2", "COMMON-LISP"),
("LAMBDA-PARAMETERS-LIMIT", "ACL2", "COMMON-LISP"),
("LOGAND", "ACL2", "COMMON-LISP"),
("LAST", "ACL2", "COMMON-LISP"),
("LOGANDC1", "ACL2", "COMMON-LISP"),
("LCM", "ACL2", "COMMON-LISP"),
("LOGANDC2", "ACL2", "COMMON-LISP"),
("LDB", "ACL2", "COMMON-LISP"),
("LOGBITP", "ACL2", "COMMON-LISP"),
("LDB-TEST", "ACL2", "COMMON-LISP"),
("LOGCOUNT", "ACL2", "COMMON-LISP"),
("LDIFF", "ACL2", "COMMON-LISP"),
("LOGEQV", "ACL2", "COMMON-LISP"),
("LEAST-NEGATIVE-DOUBLE-FLOAT", "ACL2", "COMMON-LISP"),
("LOGICAL-PATHNAME", "ACL2", "COMMON-LISP"),
("LEAST-NEGATIVE-LONG-FLOAT", "ACL2", "COMMON-LISP"),
("LOGICAL-PATHNAME-TRANSLATIONS", "ACL2", "COMMON-LISP"),
("LEAST-NEGATIVE-NORMALIZED-DOUBLE-FLOAT", "ACL2", "COMMON-LISP"),
("LOGIOR", "ACL2", "COMMON-LISP"),
("LEAST-NEGATIVE-NORMALIZED-LONG-FLOAT", "ACL2", "COMMON-LISP"),
("LOGNAND", "ACL2", "COMMON-LISP"),
("LEAST-NEGATIVE-NORMALIZED-SHORT-FLOAT", "ACL2", "COMMON-LISP"),
("LOGNOR", "ACL2", "COMMON-LISP"),
("LEAST-NEGATIVE-NORMALIZED-SINGLE-FLOAT", "ACL2", "COMMON-LISP"),
("LOGNOT", "ACL2", "COMMON-LISP"),
("LEAST-NEGATIVE-SHORT-FLOAT", "ACL2", "COMMON-LISP"),
("LOGORC1", "ACL2", "COMMON-LISP"),
("LEAST-NEGATIVE-SINGLE-FLOAT", "ACL2", "COMMON-LISP"),
("LOGORC2", "ACL2", "COMMON-LISP"),
("LEAST-POSITIVE-DOUBLE-FLOAT", "ACL2", "COMMON-LISP"),
("LOGTEST", "ACL2", "COMMON-LISP"),
("LEAST-POSITIVE-LONG-FLOAT", "ACL2", "COMMON-LISP"),
("LOGXOR", "ACL2", "COMMON-LISP"),
("LEAST-POSITIVE-NORMALIZED-DOUBLE-FLOAT", "ACL2", "COMMON-LISP"),
("LONG-FLOAT", "ACL2", "COMMON-LISP"),
("LEAST-POSITIVE-NORMALIZED-LONG-FLOAT", "ACL2", "COMMON-LISP"),
("LONG-FLOAT-EPSILON", "ACL2", "COMMON-LISP"),
("LEAST-POSITIVE-NORMALIZED-SHORT-FLOAT", "ACL2", "COMMON-LISP"),
("LONG-FLOAT-NEGATIVE-EPSILON", "ACL2", "COMMON-LISP"),
("LEAST-POSITIVE-NORMALIZED-SINGLE-FLOAT", "ACL2", "COMMON-LISP"),
("LONG-SITE-NAME", "ACL2", "COMMON-LISP"),
("LEAST-POSITIVE-SHORT-FLOAT", "ACL2", "COMMON-LISP"),
("LOOP", "ACL2", "COMMON-LISP"),
("LEAST-POSITIVE-SINGLE-FLOAT", "ACL2", "COMMON-LISP"),
("LOOP-FINISH", "ACL2", "COMMON-LISP"),
("LENGTH", "ACL2", "COMMON-LISP"),
("LOWER-CASE-P", "ACL2", "COMMON-LISP"),
("LET", "ACL2", "COMMON-LISP"),
("MACHINE-INSTANCE", "ACL2", "COMMON-LISP"),
("LET*", "ACL2", "COMMON-LISP"),
("MACHINE-TYPE", "ACL2", "COMMON-LISP"),
("MACHINE-VERSION", "ACL2", "COMMON-LISP"),
("MASK-FIELD", "ACL2", "COMMON-LISP"),
("MACRO-FUNCTION", "ACL2", "COMMON-LISP"),
("MAX", "ACL2", "COMMON-LISP"),
("MACROEXPAND", "ACL2", "COMMON-LISP"),
("MEMBER", "ACL2", "COMMON-LISP"),
("MACROEXPAND-1", "ACL2", "COMMON-LISP"),
("MEMBER-IF", "ACL2", "COMMON-LISP"),
("MACROLET", "ACL2", "COMMON-LISP"),
("MEMBER-IF-NOT", "ACL2", "COMMON-LISP"),
("MAKE-ARRAY", "ACL2", "COMMON-LISP"),
("MERGE", "ACL2", "COMMON-LISP"),
("MAKE-BROADCAST-STREAM", "ACL2", "COMMON-LISP"),
("MERGE-PATHNAMES", "ACL2", "COMMON-LISP"),
("MAKE-CONCATENATED-STREAM", "ACL2", "COMMON-LISP"),
("METHOD", "ACL2", "COMMON-LISP"),
("MAKE-CONDITION", "ACL2", "COMMON-LISP"),
("METHOD-COMBINATION", "ACL2", "COMMON-LISP"),
("MAKE-DISPATCH-MACRO-CHARACTER", "ACL2", "COMMON-LISP"),
("METHOD-COMBINATION-ERROR", "ACL2", "COMMON-LISP"),
("MAKE-ECHO-STREAM", "ACL2", "COMMON-LISP"),
("METHOD-QUALIFIERS", "ACL2", "COMMON-LISP"),
("MAKE-HASH-TABLE", "ACL2", "COMMON-LISP"),
("MIN", "ACL2", "COMMON-LISP"),
("MAKE-INSTANCE", "ACL2", "COMMON-LISP"),
("MINUSP", "ACL2", "COMMON-LISP"),
("MAKE-INSTANCES-OBSOLETE", "ACL2", "COMMON-LISP"),
("MISMATCH", "ACL2", "COMMON-LISP"),
("MAKE-LIST", "ACL2", "COMMON-LISP"),
("MOD", "ACL2", "COMMON-LISP"),
("MAKE-LOAD-FORM", "ACL2", "COMMON-LISP"),
("MOST-NEGATIVE-DOUBLE-FLOAT", "ACL2", "COMMON-LISP"),
("MAKE-LOAD-FORM-SAVING-SLOTS", "ACL2", "COMMON-LISP"),
("MOST-NEGATIVE-FIXNUM", "ACL2", "COMMON-LISP"),
("MAKE-METHOD", "ACL2", "COMMON-LISP"),
("MOST-NEGATIVE-LONG-FLOAT", "ACL2", "COMMON-LISP"),
("MAKE-PACKAGE", "ACL2", "COMMON-LISP"),
("MOST-NEGATIVE-SHORT-FLOAT", "ACL2", "COMMON-LISP"),
("MAKE-PATHNAME", "ACL2", "COMMON-LISP"),
("MOST-NEGATIVE-SINGLE-FLOAT", "ACL2", "COMMON-LISP"),
("MAKE-RANDOM-STATE", "ACL2", "COMMON-LISP"),
("MOST-POSITIVE-DOUBLE-FLOAT", "ACL2", "COMMON-LISP"),
("MAKE-SEQUENCE", "ACL2", "COMMON-LISP"),
("MOST-POSITIVE-FIXNUM", "ACL2", "COMMON-LISP"),
("MAKE-STRING", "ACL2", "COMMON-LISP"),
("MOST-POSITIVE-LONG-FLOAT", "ACL2", "COMMON-LISP"),
("MAKE-STRING-INPUT-STREAM", "ACL2", "COMMON-LISP"),
("MOST-POSITIVE-SHORT-FLOAT", "ACL2", "COMMON-LISP"),
("MAKE-STRING-OUTPUT-STREAM", "ACL2", "COMMON-LISP"),
("MOST-POSITIVE-SINGLE-FLOAT", "ACL2", "COMMON-LISP"),
("MAKE-SYMBOL", "ACL2", "COMMON-LISP"),
("MUFFLE-WARNING", "ACL2", "COMMON-LISP"),
("MAKE-SYNONYM-STREAM", "ACL2", "COMMON-LISP"),
("MULTIPLE-VALUE-BIND", "ACL2", "COMMON-LISP"),
("MAKE-TWO-WAY-STREAM", "ACL2", "COMMON-LISP"),
("MULTIPLE-VALUE-CALL", "ACL2", "COMMON-LISP"),
("MAKUNBOUND", "ACL2", "COMMON-LISP"),
("MULTIPLE-VALUE-LIST", "ACL2", "COMMON-LISP"),
("MAP", "ACL2", "COMMON-LISP"),
("MULTIPLE-VALUE-PROG1", "ACL2", "COMMON-LISP"),
("MAP-INTO", "ACL2", "COMMON-LISP"),
("MULTIPLE-VALUE-SETQ", "ACL2", "COMMON-LISP"),
("MAPC", "ACL2", "COMMON-LISP"),
("MULTIPLE-VALUES-LIMIT", "ACL2", "COMMON-LISP"),
("MAPCAN", "ACL2", "COMMON-LISP"),
("NAME-CHAR", "ACL2", "COMMON-LISP"),
("MAPCAR", "ACL2", "COMMON-LISP"),
("NAMESTRING", "ACL2", "COMMON-LISP"),
("MAPCON", "ACL2", "COMMON-LISP"),
("NBUTLAST", "ACL2", "COMMON-LISP"),
("MAPHASH", "ACL2", "COMMON-LISP"),
("NCONC", "ACL2", "COMMON-LISP"),
("MAPL", "ACL2", "COMMON-LISP"),
("NEXT-METHOD-P", "ACL2", "COMMON-LISP"),
("MAPLIST", "ACL2", "COMMON-LISP"),
("NIL", "ACL2", "COMMON-LISP"),
("NINTERSECTION", "ACL2", "COMMON-LISP"),
("PACKAGE-ERROR", "ACL2", "COMMON-LISP"),
("NINTH", "ACL2", "COMMON-LISP"),
("PACKAGE-ERROR-PACKAGE", "ACL2", "COMMON-LISP"),
("NO-APPLICABLE-METHOD", "ACL2", "COMMON-LISP"),
("PACKAGE-NAME", "ACL2", "COMMON-LISP"),
("NO-NEXT-METHOD", "ACL2", "COMMON-LISP"),
("PACKAGE-NICKNAMES", "ACL2", "COMMON-LISP"),
("NOT", "ACL2", "COMMON-LISP"),
("PACKAGE-SHADOWING-SYMBOLS", "ACL2", "COMMON-LISP"),
("NOTANY", "ACL2", "COMMON-LISP"),
("PACKAGE-USE-LIST", "ACL2", "COMMON-LISP"),
("NOTEVERY", "ACL2", "COMMON-LISP"),
("PACKAGE-USED-BY-LIST", "ACL2", "COMMON-LISP"),
("NOTINLINE", "ACL2", "COMMON-LISP"),
("PACKAGEP", "ACL2", "COMMON-LISP"),
("NRECONC", "ACL2", "COMMON-LISP"),
("PAIRLIS", "ACL2", "COMMON-LISP"),
("NREVERSE", "ACL2", "COMMON-LISP"),
("PARSE-ERROR", "ACL2", "COMMON-LISP"),
("NSET-DIFFERENCE", "ACL2", "COMMON-LISP"),
("PARSE-INTEGER", "ACL2", "COMMON-LISP"),
("NSET-EXCLUSIVE-OR", "ACL2", "COMMON-LISP"),
("PARSE-NAMESTRING", "ACL2", "COMMON-LISP"),
("NSTRING-CAPITALIZE", "ACL2", "COMMON-LISP"),
("PATHNAME", "ACL2", "COMMON-LISP"),
("NSTRING-DOWNCASE", "ACL2", "COMMON-LISP"),
("PATHNAME-DEVICE", "ACL2", "COMMON-LISP"),
("NSTRING-UPCASE", "ACL2", "COMMON-LISP"),
("PATHNAME-DIRECTORY", "ACL2", "COMMON-LISP"),
("NSUBLIS", "ACL2", "COMMON-LISP"),
("PATHNAME-HOST", "ACL2", "COMMON-LISP"),
("NSUBST", "ACL2", "COMMON-LISP"),
("PATHNAME-MATCH-P", "ACL2", "COMMON-LISP"),
("NSUBST-IF", "ACL2", "COMMON-LISP"),
("PATHNAME-NAME", "ACL2", "COMMON-LISP"),
("NSUBST-IF-NOT", "ACL2", "COMMON-LISP"),
("PATHNAME-TYPE", "ACL2", "COMMON-LISP"),
("NSUBSTITUTE", "ACL2", "COMMON-LISP"),
("PATHNAME-VERSION", "ACL2", "COMMON-LISP"),
("NSUBSTITUTE-IF", "ACL2", "COMMON-LISP"),
("PATHNAMEP", "ACL2", "COMMON-LISP"),
("NSUBSTITUTE-IF-NOT", "ACL2", "COMMON-LISP"),
("PEEK-CHAR", "ACL2", "COMMON-LISP"),
("NTH", "ACL2", "COMMON-LISP"),
("PHASE", "ACL2", "COMMON-LISP"),
("NTH-VALUE", "ACL2", "COMMON-LISP"),
("PI", "ACL2", "COMMON-LISP"),
("NTHCDR", "ACL2", "COMMON-LISP"),
("PLUSP", "ACL2", "COMMON-LISP"),
("NULL", "ACL2", "COMMON-LISP"),
("POP", "ACL2", "COMMON-LISP"),
("NUMBER", "ACL2", "COMMON-LISP"),
("POSITION", "ACL2", "COMMON-LISP"),
("NUMBERP", "ACL2", "COMMON-LISP"),
("POSITION-IF", "ACL2", "COMMON-LISP"),
("NUMERATOR", "ACL2", "COMMON-LISP"),
("POSITION-IF-NOT", "ACL2", "COMMON-LISP"),
("NUNION", "ACL2", "COMMON-LISP"),
("PPRINT", "ACL2", "COMMON-LISP"),
("ODDP", "ACL2", "COMMON-LISP"),
("PPRINT-DISPATCH", "ACL2", "COMMON-LISP"),
("OPEN", "ACL2", "COMMON-LISP"),
("PPRINT-EXIT-IF-LIST-EXHAUSTED", "ACL2", "COMMON-LISP"),
("OPEN-STREAM-P", "ACL2", "COMMON-LISP"),
("PPRINT-FILL", "ACL2", "COMMON-LISP"),
("OPTIMIZE", "ACL2", "COMMON-LISP"),
("PPRINT-INDENT", "ACL2", "COMMON-LISP"),
("OR", "ACL2", "COMMON-LISP"),
("PPRINT-LINEAR", "ACL2", "COMMON-LISP"),
("OTHERWISE", "ACL2", "COMMON-LISP"),
("PPRINT-LOGICAL-BLOCK", "ACL2", "COMMON-LISP"),
("OUTPUT-STREAM-P", "ACL2", "COMMON-LISP"),
("PPRINT-NEWLINE", "ACL2", "COMMON-LISP"),
("PACKAGE", "ACL2", "COMMON-LISP"),
("PPRINT-POP", "ACL2", "COMMON-LISP"),
("PPRINT-TAB", "ACL2", "COMMON-LISP"),
("READ-CHAR", "ACL2", "COMMON-LISP"),
("PPRINT-TABULAR", "ACL2", "COMMON-LISP"),
("READ-CHAR-NO-HANG", "ACL2", "COMMON-LISP"),
("PRIN1", "ACL2", "COMMON-LISP"),
("READ-DELIMITED-LIST", "ACL2", "COMMON-LISP"),
("PRIN1-TO-STRING", "ACL2", "COMMON-LISP"),
("READ-FROM-STRING", "ACL2", "COMMON-LISP"),
("PRINC", "ACL2", "COMMON-LISP"),
("READ-LINE", "ACL2", "COMMON-LISP"),
("PRINC-TO-STRING", "ACL2", "COMMON-LISP"),
("READ-PRESERVING-WHITESPACE", "ACL2", "COMMON-LISP"),
("PRINT", "ACL2", "COMMON-LISP"),
("READ-SEQUENCE", "ACL2", "COMMON-LISP"),
("PRINT-NOT-READABLE", "ACL2", "COMMON-LISP"),
("READER-ERROR", "ACL2", "COMMON-LISP"),
("PRINT-NOT-READABLE-OBJECT", "ACL2", "COMMON-LISP"),
("READTABLE", "ACL2", "COMMON-LISP"),
("PRINT-OBJECT", "ACL2", "COMMON-LISP"),
("READTABLE-CASE", "ACL2", "COMMON-LISP"),
("PRINT-UNREADABLE-OBJECT", "ACL2", "COMMON-LISP"),
("READTABLEP", "ACL2", "COMMON-LISP"),
("PROBE-FILE", "ACL2", "COMMON-LISP"),
("REAL", "ACL2", "COMMON-LISP"),
("PROCLAIM", "ACL2", "COMMON-LISP"),
("REALP", "ACL2", "COMMON-LISP"),
("PROG", "ACL2", "COMMON-LISP"),
("REALPART", "ACL2", "COMMON-LISP"),
("PROG*", "ACL2", "COMMON-LISP"),
("REDUCE", "ACL2", "COMMON-LISP"),
("PROG1", "ACL2", "COMMON-LISP"),
("REINITIALIZE-INSTANCE", "ACL2", "COMMON-LISP"),
("PROG2", "ACL2", "COMMON-LISP"),
("REM", "ACL2", "COMMON-LISP"),
("PROGN", "ACL2", "COMMON-LISP"),
("REMF", "ACL2", "COMMON-LISP"),
("PROGRAM-ERROR", "ACL2", "COMMON-LISP"),
("REMHASH", "ACL2", "COMMON-LISP"),
("PROGV", "ACL2", "COMMON-LISP"),
("REMOVE", "ACL2", "COMMON-LISP"),
("PROVIDE", "ACL2", "COMMON-LISP"),
("REMOVE-DUPLICATES", "ACL2", "COMMON-LISP"),
("PSETF", "ACL2", "COMMON-LISP"),
("REMOVE-IF", "ACL2", "COMMON-LISP"),
("PSETQ", "ACL2", "COMMON-LISP"),
("REMOVE-IF-NOT", "ACL2", "COMMON-LISP"),
("PUSH", "ACL2", "COMMON-LISP"),
("REMOVE-METHOD", "ACL2", "COMMON-LISP"),
("PUSHNEW", "ACL2", "COMMON-LISP"),
("REMPROP", "ACL2", "COMMON-LISP"),
("QUOTE", "ACL2", "COMMON-LISP"),
("RENAME-FILE", "ACL2", "COMMON-LISP"),
("RANDOM", "ACL2", "COMMON-LISP"),
("RENAME-PACKAGE", "ACL2", "COMMON-LISP"),
("RANDOM-STATE", "ACL2", "COMMON-LISP"),
("REPLACE", "ACL2", "COMMON-LISP"),
("RANDOM-STATE-P", "ACL2", "COMMON-LISP"),
("REQUIRE", "ACL2", "COMMON-LISP"),
("RASSOC", "ACL2", "COMMON-LISP"),
("REST", "ACL2", "COMMON-LISP"),
("RASSOC-IF", "ACL2", "COMMON-LISP"),
("RESTART", "ACL2", "COMMON-LISP"),
("RASSOC-IF-NOT", "ACL2", "COMMON-LISP"),
("RESTART-BIND", "ACL2", "COMMON-LISP"),
("RATIO", "ACL2", "COMMON-LISP"),
("RESTART-CASE", "ACL2", "COMMON-LISP"),
("RATIONAL", "ACL2", "COMMON-LISP"),
("RESTART-NAME", "ACL2", "COMMON-LISP"),
("RATIONALIZE", "ACL2", "COMMON-LISP"),
("RETURN", "ACL2", "COMMON-LISP"),
("RATIONALP", "ACL2", "COMMON-LISP"),
("RETURN-FROM", "ACL2", "COMMON-LISP"),
("READ", "ACL2", "COMMON-LISP"),
("REVAPPEND", "ACL2", "COMMON-LISP"),
("READ-BYTE", "ACL2", "COMMON-LISP"),
("REVERSE", "ACL2", "COMMON-LISP"),
("ROOM", "ACL2", "COMMON-LISP"),
("SIMPLE-BIT-VECTOR", "ACL2", "COMMON-LISP"),
("ROTATEF", "ACL2", "COMMON-LISP"),
("SIMPLE-BIT-VECTOR-P", "ACL2", "COMMON-LISP"),
("ROUND", "ACL2", "COMMON-LISP"),
("SIMPLE-CONDITION", "ACL2", "COMMON-LISP"),
("ROW-MAJOR-AREF", "ACL2", "COMMON-LISP"),
("SIMPLE-CONDITION-FORMAT-ARGUMENTS", "ACL2", "COMMON-LISP"),
("RPLACA", "ACL2", "COMMON-LISP"),
("SIMPLE-CONDITION-FORMAT-CONTROL", "ACL2", "COMMON-LISP"),
("RPLACD", "ACL2", "COMMON-LISP"),
("SIMPLE-ERROR", "ACL2", "COMMON-LISP"),
("SAFETY", "ACL2", "COMMON-LISP"),
("SIMPLE-STRING", "ACL2", "COMMON-LISP"),
("SATISFIES", "ACL2", "COMMON-LISP"),
("SIMPLE-STRING-P", "ACL2", "COMMON-LISP"),
("SBIT", "ACL2", "COMMON-LISP"),
("SIMPLE-TYPE-ERROR", "ACL2", "COMMON-LISP"),
("SCALE-FLOAT", "ACL2", "COMMON-LISP"),
("SIMPLE-VECTOR", "ACL2", "COMMON-LISP"),
("SCHAR", "ACL2", "COMMON-LISP"),
("SIMPLE-VECTOR-P", "ACL2", "COMMON-LISP"),
("SEARCH", "ACL2", "COMMON-LISP"),
("SIMPLE-WARNING", "ACL2", "COMMON-LISP"),
("SECOND", "ACL2", "COMMON-LISP"),
("SIN", "ACL2", "COMMON-LISP"),
("SEQUENCE", "ACL2", "COMMON-LISP"),
("SINGLE-FLOAT", "ACL2", "COMMON-LISP"),
("SERIOUS-CONDITION", "ACL2", "COMMON-LISP"),
("SINGLE-FLOAT-EPSILON", "ACL2", "COMMON-LISP"),
("SET", "ACL2", "COMMON-LISP"),
("SINGLE-FLOAT-NEGATIVE-EPSILON", "ACL2", "COMMON-LISP"),
("SET-DIFFERENCE", "ACL2", "COMMON-LISP"),
("SINH", "ACL2", "COMMON-LISP"),
("SET-DISPATCH-MACRO-CHARACTER", "ACL2", "COMMON-LISP"),
("SIXTH", "ACL2", "COMMON-LISP"),
("SET-EXCLUSIVE-OR", "ACL2", "COMMON-LISP"),
("SLEEP", "ACL2", "COMMON-LISP"),
("SET-MACRO-CHARACTER", "ACL2", "COMMON-LISP"),
("SLOT-BOUNDP", "ACL2", "COMMON-LISP"),
("SET-PPRINT-DISPATCH", "ACL2", "COMMON-LISP"),
("SLOT-EXISTS-P", "ACL2", "COMMON-LISP"),
("SET-SYNTAX-FROM-CHAR", "ACL2", "COMMON-LISP"),
("SLOT-MAKUNBOUND", "ACL2", "COMMON-LISP"),
("SETF", "ACL2", "COMMON-LISP"),
("SLOT-MISSING", "ACL2", "COMMON-LISP"),
("SETQ", "ACL2", "COMMON-LISP"),
("SLOT-UNBOUND", "ACL2", "COMMON-LISP"),
("SEVENTH", "ACL2", "COMMON-LISP"),
("SLOT-VALUE", "ACL2", "COMMON-LISP"),
("SHADOW", "ACL2", "COMMON-LISP"),
("SOFTWARE-TYPE", "ACL2", "COMMON-LISP"),
("SHADOWING-IMPORT", "ACL2", "COMMON-LISP"),
("SOFTWARE-VERSION", "ACL2", "COMMON-LISP"),
("SHARED-INITIALIZE", "ACL2", "COMMON-LISP"),
("SOME", "ACL2", "COMMON-LISP"),
("SHIFTF", "ACL2", "COMMON-LISP"),
("SORT", "ACL2", "COMMON-LISP"),
("SHORT-FLOAT", "ACL2", "COMMON-LISP"),
("SPACE", "ACL2", "COMMON-LISP"),
("SHORT-FLOAT-EPSILON", "ACL2", "COMMON-LISP"),
("SPECIAL", "ACL2", "COMMON-LISP"),
("SHORT-FLOAT-NEGATIVE-EPSILON", "ACL2", "COMMON-LISP"),
("SPECIAL-OPERATOR-P", "ACL2", "COMMON-LISP"),
("SHORT-SITE-NAME", "ACL2", "COMMON-LISP"),
("SPEED", "ACL2", "COMMON-LISP"),
("SIGNAL", "ACL2", "COMMON-LISP"),
("SQRT", "ACL2", "COMMON-LISP"),
("SIGNED-BYTE", "ACL2", "COMMON-LISP"),
("STABLE-SORT", "ACL2", "COMMON-LISP"),
("SIGNUM", "ACL2", "COMMON-LISP"),
("STANDARD", "ACL2", "COMMON-LISP"),
("SIMPLE-ARRAY", "ACL2", "COMMON-LISP"),
("STANDARD-CHAR", "ACL2", "COMMON-LISP"),
("SIMPLE-BASE-STRING", "ACL2", "COMMON-LISP"),
("STANDARD-CHAR-P", "ACL2", "COMMON-LISP"),
("STANDARD-CLASS", "ACL2", "COMMON-LISP"),
("SUBLIS", "ACL2", "COMMON-LISP"),
("STANDARD-GENERIC-FUNCTION", "ACL2", "COMMON-LISP"),
("SUBSEQ", "ACL2", "COMMON-LISP"),
("STANDARD-METHOD", "ACL2", "COMMON-LISP"),
("SUBSETP", "ACL2", "COMMON-LISP"),
("STANDARD-OBJECT", "ACL2", "COMMON-LISP"),
("SUBST", "ACL2", "COMMON-LISP"),
("STEP", "ACL2", "COMMON-LISP"),
("SUBST-IF", "ACL2", "COMMON-LISP"),
("STORAGE-CONDITION", "ACL2", "COMMON-LISP"),
("SUBST-IF-NOT", "ACL2", "COMMON-LISP"),
("STORE-VALUE", "ACL2", "COMMON-LISP"),
("SUBSTITUTE", "ACL2", "COMMON-LISP"),
("STREAM", "ACL2", "COMMON-LISP"),
("SUBSTITUTE-IF", "ACL2", "COMMON-LISP"),
("STREAM-ELEMENT-TYPE", "ACL2", "COMMON-LISP"),
("SUBSTITUTE-IF-NOT", "ACL2", "COMMON-LISP"),
("STREAM-ERROR", "ACL2", "COMMON-LISP"),
("SUBTYPEP", "ACL2", "COMMON-LISP"),
("STREAM-ERROR-STREAM", "ACL2", "COMMON-LISP"),
("SVREF", "ACL2", "COMMON-LISP"),
("STREAM-EXTERNAL-FORMAT", "ACL2", "COMMON-LISP"),
("SXHASH", "ACL2", "COMMON-LISP"),
("STREAMP", "ACL2", "COMMON-LISP"),
("SYMBOL", "ACL2", "COMMON-LISP"),
("STRING", "ACL2", "COMMON-LISP"),
("SYMBOL-FUNCTION", "ACL2", "COMMON-LISP"),
("STRING-CAPITALIZE", "ACL2", "COMMON-LISP"),
("SYMBOL-MACROLET", "ACL2", "COMMON-LISP"),
("STRING-DOWNCASE", "ACL2", "COMMON-LISP"),
("SYMBOL-NAME", "ACL2", "COMMON-LISP"),
("STRING-EQUAL", "ACL2", "COMMON-LISP"),
("SYMBOL-PACKAGE", "ACL2", "COMMON-LISP"),
("STRING-GREATERP", "ACL2", "COMMON-LISP"),
("SYMBOL-PLIST", "ACL2", "COMMON-LISP"),
("STRING-LEFT-TRIM", "ACL2", "COMMON-LISP"),
("SYMBOL-VALUE", "ACL2", "COMMON-LISP"),
("STRING-LESSP", "ACL2", "COMMON-LISP"),
("SYMBOLP", "ACL2", "COMMON-LISP"),
("STRING-NOT-EQUAL", "ACL2", "COMMON-LISP"),
("SYNONYM-STREAM", "ACL2", "COMMON-LISP"),
("STRING-NOT-GREATERP", "ACL2", "COMMON-LISP"),
("SYNONYM-STREAM-SYMBOL", "ACL2", "COMMON-LISP"),
("STRING-NOT-LESSP", "ACL2", "COMMON-LISP"),
("T", "ACL2", "COMMON-LISP"),
("STRING-RIGHT-TRIM", "ACL2", "COMMON-LISP"),
("TAGBODY", "ACL2", "COMMON-LISP"),
("STRING-STREAM", "ACL2", "COMMON-LISP"),
("TAILP", "ACL2", "COMMON-LISP"),
("STRING-TRIM", "ACL2", "COMMON-LISP"),
("TAN", "ACL2", "COMMON-LISP"),
("STRING-UPCASE", "ACL2", "COMMON-LISP"),
("TANH", "ACL2", "COMMON-LISP"),
("STRING/=", "ACL2", "COMMON-LISP"),
("TENTH", "ACL2", "COMMON-LISP"),
("STRING<", "ACL2", "COMMON-LISP"),
("TERPRI", "ACL2", "COMMON-LISP"),
("STRING<=", "ACL2", "COMMON-LISP"),
("THE", "ACL2", "COMMON-LISP"),
("STRING=", "ACL2", "COMMON-LISP"),
("THIRD", "ACL2", "COMMON-LISP"),
("STRING>", "ACL2", "COMMON-LISP"),
("THROW", "ACL2", "COMMON-LISP"),
("STRING>=", "ACL2", "COMMON-LISP"),
("TIME", "ACL2", "COMMON-LISP"),
("STRINGP", "ACL2", "COMMON-LISP"),
("TRACE", "ACL2", "COMMON-LISP"),
("STRUCTURE", "ACL2", "COMMON-LISP"),
("TRANSLATE-LOGICAL-PATHNAME", "ACL2", "COMMON-LISP"),
("STRUCTURE-CLASS", "ACL2", "COMMON-LISP"),
("TRANSLATE-PATHNAME", "ACL2", "COMMON-LISP"),
("STRUCTURE-OBJECT", "ACL2", "COMMON-LISP"),
("TREE-EQUAL", "ACL2", "COMMON-LISP"),
("STYLE-WARNING", "ACL2", "COMMON-LISP"),
("TRUENAME", "ACL2", "COMMON-LISP"),
("TRUNCATE", "ACL2", "COMMON-LISP"),
("VALUES-LIST", "ACL2", "COMMON-LISP"),
("TWO-WAY-STREAM", "ACL2", "COMMON-LISP"),
("VARIABLE", "ACL2", "COMMON-LISP"),
("TWO-WAY-STREAM-INPUT-STREAM", "ACL2", "COMMON-LISP"),
("VECTOR", "ACL2", "COMMON-LISP"),
("TWO-WAY-STREAM-OUTPUT-STREAM", "ACL2", "COMMON-LISP"),
("VECTOR-POP", "ACL2", "COMMON-LISP"),
("TYPE", "ACL2", "COMMON-LISP"),
("VECTOR-PUSH", "ACL2", "COMMON-LISP"),
("TYPE-ERROR", "ACL2", "COMMON-LISP"),
("VECTOR-PUSH-EXTEND", "ACL2", "COMMON-LISP"),
("TYPE-ERROR-DATUM", "ACL2", "COMMON-LISP"),
("VECTORP", "ACL2", "COMMON-LISP"),
("TYPE-ERROR-EXPECTED-TYPE", "ACL2", "COMMON-LISP"),
("WARN", "ACL2", "COMMON-LISP"),
("TYPE-OF", "ACL2", "COMMON-LISP"),
("WARNING", "ACL2", "COMMON-LISP"),
("TYPECASE", "ACL2", "COMMON-LISP"),
("WHEN", "ACL2", "COMMON-LISP"),
("TYPEP", "ACL2", "COMMON-LISP"),
("WILD-PATHNAME-P", "ACL2", "COMMON-LISP"),
("UNBOUND-SLOT", "ACL2", "COMMON-LISP"),
("WITH-ACCESSORS", "ACL2", "COMMON-LISP"),
("UNBOUND-SLOT-INSTANCE", "ACL2", "COMMON-LISP"),
("WITH-COMPILATION-UNIT", "ACL2", "COMMON-LISP"),
("UNBOUND-VARIABLE", "ACL2", "COMMON-LISP"),
("WITH-CONDITION-RESTARTS", "ACL2", "COMMON-LISP"),
("UNDEFINED-FUNCTION", "ACL2", "COMMON-LISP"),
("WITH-HASH-TABLE-ITERATOR", "ACL2", "COMMON-LISP"),
("UNEXPORT", "ACL2", "COMMON-LISP"),
("WITH-INPUT-FROM-STRING", "ACL2", "COMMON-LISP"),
("UNINTERN", "ACL2", "COMMON-LISP"),
("WITH-OPEN-FILE", "ACL2", "COMMON-LISP"),
("UNION", "ACL2", "COMMON-LISP"),
("WITH-OPEN-STREAM", "ACL2", "COMMON-LISP"),
("UNLESS", "ACL2", "COMMON-LISP"),
("WITH-OUTPUT-TO-STRING", "ACL2", "COMMON-LISP"),
("UNREAD-CHAR", "ACL2", "COMMON-LISP"),
("WITH-PACKAGE-ITERATOR", "ACL2", "COMMON-LISP"),
("UNSIGNED-BYTE", "ACL2", "COMMON-LISP"),
("WITH-SIMPLE-RESTART", "ACL2", "COMMON-LISP"),
("UNTRACE", "ACL2", "COMMON-LISP"),
("WITH-SLOTS", "ACL2", "COMMON-LISP"),
("UNUSE-PACKAGE", "ACL2", "COMMON-LISP"),
("WITH-STANDARD-IO-SYNTAX", "ACL2", "COMMON-LISP"),
("UNWIND-PROTECT", "ACL2", "COMMON-LISP"),
("WRITE", "ACL2", "COMMON-LISP"),
("UPDATE-INSTANCE-FOR-DIFFERENT-CLASS", "ACL2", "COMMON-LISP"),
("WRITE-BYTE", "ACL2", "COMMON-LISP"),
("UPDATE-INSTANCE-FOR-REDEFINED-CLASS", "ACL2", "COMMON-LISP"),
("WRITE-CHAR", "ACL2", "COMMON-LISP"),
("UPGRADED-ARRAY-ELEMENT-TYPE", "ACL2", "COMMON-LISP"),
("WRITE-LINE", "ACL2", "COMMON-LISP"),
("UPGRADED-COMPLEX-PART-TYPE", "ACL2", "COMMON-LISP"),
("WRITE-SEQUENCE", "ACL2", "COMMON-LISP"),
("UPPER-CASE-P", "ACL2", "COMMON-LISP"),
("WRITE-STRING", "ACL2", "COMMON-LISP"),
("USE-PACKAGE", "ACL2", "COMMON-LISP"),
("WRITE-TO-STRING", "ACL2", "COMMON-LISP"),
("USE-VALUE", "ACL2", "COMMON-LISP"),
("Y-OR-N-P", "ACL2", "COMMON-LISP"),
("USER-HOMEDIR-PATHNAME", "ACL2", "COMMON-LISP"),
("YES-OR-NO-P", "ACL2", "COMMON-LISP"),
("VALUES", "ACL2", "COMMON-LISP"),
("ZEROP", "ACL2", "COMMON-LISP")
]