1176998Sphk 2176998SphkACL2_PACKAGE_STRUCTURE := 3176998Sphk[ 4176998Sphk("&", "ACL2-USER", "ACL2"), 5176998Sphk("*ACL2-EXPORTS*", "ACL2-USER", "ACL2"), 6176998Sphk("*COMMON-LISP-SPECIALS-AND-CONSTANTS*", "ACL2-USER", "ACL2"), 7176998Sphk("*COMMON-LISP-SYMBOLS-FROM-MAIN-LISP-PACKAGE*", "ACL2-USER", "ACL2"), 8176998Sphk("*MAIN-LISP-PACKAGE-NAME*", "ACL2-USER", "ACL2"), 9176998Sphk("*STANDARD-CHARS*", "ACL2-USER", "ACL2"), 10176998Sphk("*STANDARD-CI*", "ACL2-USER", "ACL2"), 11176998Sphk("*STANDARD-CO*", "ACL2-USER", "ACL2"), 12176998Sphk("*STANDARD-OI*", "ACL2-USER", "ACL2"), 13176998Sphk("32-BIT-INTEGER-LISTP", "ACL2-USER", "ACL2"), 14176998Sphk("32-BIT-INTEGER-LISTP-FORWARD-TO-INTEGER-LISTP", "ACL2-USER", "ACL2"), 15176998Sphk("32-BIT-INTEGER-STACK", "ACL2-USER", "ACL2"), 16176998Sphk("32-BIT-INTEGER-STACK-LENGTH", "ACL2-USER", "ACL2"), 17176998Sphk("32-BIT-INTEGER-STACK-LENGTH1", "ACL2-USER", "ACL2"), 18176998Sphk("32-BIT-INTEGERP", "ACL2-USER", "ACL2"), 19176998Sphk("32-BIT-INTEGERP-FORWARD-TO-INTEGERP", "ACL2-USER", "ACL2"), 20176998Sphk("<-ON-OTHERS", "ACL2-USER", "ACL2"), 21176998Sphk("?-FN", "ACL2-USER", "ACL2"), 22176998Sphk("@", "ACL2-USER", "ACL2"), 23176998Sphk("ABORT!", "ACL2-USER", "ACL2"), 24176998Sphk("ACCUMULATED-PERSISTENCE", "ACL2-USER", "ACL2"), 25176998Sphk("ACL2-COUNT", "ACL2-USER", "ACL2"), 26176998Sphk("ACL2-INPUT-CHANNEL-PACKAGE", "ACL2-USER", "ACL2"), 27176998Sphk("ACL2-NUMBERP", "ACL2-USER", "ACL2"), 28176998Sphk("ACL2-OUTPUT-CHANNEL-PACKAGE", "ACL2-USER", "ACL2"), 29176998Sphk("ACL2-PACKAGE", "ACL2-USER", "ACL2"), 30176998Sphk("ADD-DEFAULT-HINTS", "ACL2-USER", "ACL2"), 31179000Sphk("ADD-DEFAULT-HINTS!", "ACL2-USER", "ACL2"), 32176998Sphk("ADD-INVISIBLE-FNS", "ACL2-USER", "ACL2"), 33176998Sphk("ADD-MACRO-ALIAS", "ACL2-USER", "ACL2"), 34176998Sphk("ADD-NTH-ALIAS", "ACL2-USER", "ACL2"), 35176998Sphk("ADD-PAIR", "ACL2-USER", "ACL2"), 36176998Sphk("ADD-PAIR-PRESERVES-ALL-BOUNDP", "ACL2-USER", "ACL2"), 37176998Sphk("ADD-TIMERS", "ACL2-USER", "ACL2"), 38176998Sphk("ADD-TO-SET-EQ", "ACL2-USER", "ACL2"), 39176998Sphk("ADD-TO-SET-EQL", "ACL2-USER", "ACL2"), 40176998Sphk("ADD-TO-SET-EQUAL", "ACL2-USER", "ACL2"), 41176998Sphk("ALISTP", "ACL2-USER", "ACL2"), 42179000Sphk("ALISTP-FORWARD-TO-TRUE-LISTP", "ACL2-USER", "ACL2"), 43179000Sphk("ALL-BOUNDP", "ACL2-USER", "ACL2"), 44179000Sphk("ALL-BOUNDP-PRESERVES-ASSOC", "ACL2-USER", "ACL2"), 45219095Sphk("ALL-VARS", "ACL2-USER", "ACL2"), 46219095Sphk("ALL-VARS1", "ACL2-USER", "ACL2"), 47179000Sphk("ALL-VARS1-LST", "ACL2-USER", "ACL2"), 48179000Sphk("ALPHA-CHAR-P-FORWARD-TO-CHARACTERP", "ACL2-USER", "ACL2"), 49179000Sphk("AND-MACRO", "ACL2-USER", "ACL2"), 50179000Sphk("AREF-32-BIT-INTEGER-STACK", "ACL2-USER", "ACL2"), 51176998Sphk("AREF-T-STACK", "ACL2-USER", "ACL2"), 52176998Sphk("AREF1", "ACL2-USER", "ACL2"), 53176998Sphk("AREF2", "ACL2-USER", "ACL2"), 54176998Sphk("ARGS", "ACL2-USER", "ACL2"), 55176998Sphk("ARRAY1P", "ACL2-USER", "ACL2"), 56176998Sphk("ARRAY1P-CONS", "ACL2-USER", "ACL2"), 57176998Sphk("ARRAY1P-FORWARD", "ACL2-USER", "ACL2"), 58176998Sphk("ARRAY1P-LINEAR", "ACL2-USER", "ACL2"), 59176998Sphk("ARRAY2P", "ACL2-USER", "ACL2"), 60176998Sphk("ARRAY2P-CONS", "ACL2-USER", "ACL2"), 61176998Sphk("ARRAY2P-FORWARD", "ACL2-USER", "ACL2"), 62176998Sphk("ARRAY2P-LINEAR", "ACL2-USER", "ACL2"), 63176998Sphk("ASET-32-BIT-INTEGER-STACK", "ACL2-USER", "ACL2"), 64176998Sphk("ASET-T-STACK", "ACL2-USER", "ACL2"), 65176998Sphk("ASET1", "ACL2-USER", "ACL2"), 66176998Sphk("ASET2", "ACL2-USER", "ACL2"), 67176998Sphk("ASSIGN", "ACL2-USER", "ACL2"), 68176998Sphk("ASSOC-ADD-PAIR", "ACL2-USER", "ACL2"), 69176998Sphk("ASSOC-EQ", "ACL2-USER", "ACL2"), 70176998Sphk("ASSOC-EQ-EQUAL", "ACL2-USER", "ACL2"), 71176998Sphk("ASSOC-EQ-EQUAL-ALISTP", "ACL2-USER", "ACL2"), 72176998Sphk("ASSOC-EQUAL", "ACL2-USER", "ACL2"), 73176998Sphk("ASSOC-KEYWORD", "ACL2-USER", "ACL2"), 74176998Sphk("ASSOC-STRING-EQUAL", "ACL2-USER", "ACL2"), 75179000Sphk("ASSOC2", "ACL2-USER", "ACL2"), 76176998Sphk("ASSOCIATIVITY-OF-*", "ACL2-USER", "ACL2"), 77176998Sphk("ASSOCIATIVITY-OF-+", "ACL2-USER", "ACL2"), 78176998Sphk("ASSUME", "ACL2-USER", "ACL2"), 79176998Sphk("ATOM-LISTP", "ACL2-USER", "ACL2"), 80219027Sphk("ATOM-LISTP-FORWARD-TO-TRUE-LISTP", "ACL2-USER", "ACL2"), 81179000Sphk("BIG-CLOCK-ENTRY", "ACL2-USER", "ACL2"), 82176998Sphk("BIG-CLOCK-NEGATIVE-P", "ACL2-USER", "ACL2"), 83176998Sphk("BINARY-*", "ACL2-USER", "ACL2"), 84179000Sphk("BINARY-+", "ACL2-USER", "ACL2"), 85176998Sphk("BINARY-APPEND", "ACL2-USER", "ACL2"), 86176998Sphk("BIND-FREE", "ACL2-USER", "ACL2"), 87179000Sphk("BINOP-TABLE", "ACL2-USER", "ACL2"), 88176998Sphk("ADD-BINOP", "ACL2-USER", "ACL2"), 89176998Sphk("REMOVE-BINOP", "ACL2-USER", "ACL2"), 90176998Sphk("REMOVE-INVISIBLE-FNS", "ACL2-USER", "ACL2"), 91176998Sphk("BOOLEAN-LISTP", "ACL2-USER", "ACL2"), 92176998Sphk("BOOLEAN-LISTP-CONS", "ACL2-USER", "ACL2"), 93176998Sphk("BOOLEAN-LISTP-FORWARD", "ACL2-USER", "ACL2"), 94176998Sphk("BOOLEAN-LISTP-FORWARD-TO-SYMBOL-LISTP", "ACL2-USER", "ACL2"), 95176998Sphk("BOOLEANP", "ACL2-USER", "ACL2"), 96176998Sphk("BOOLEANP-CHARACTERP", "ACL2-USER", "ACL2"), 97176998Sphk("BOOLEANP-COMPOUND-RECOGNIZER", "ACL2-USER", "ACL2"), 98176998Sphk("BOUNDED-INTEGER-ALISTP", "ACL2-USER", "ACL2"), 99176998Sphk("BOUNDED-INTEGER-ALISTP-FORWARD-TO-EQLABLE-ALISTP", "ACL2-USER", "ACL2"), 100176998Sphk("BOUNDED-INTEGER-ALISTP2", "ACL2-USER", "ACL2"), 101176998Sphk("BOUNDP-GLOBAL", "ACL2-USER", "ACL2"), 102176998Sphk("BOUNDP-GLOBAL1", "ACL2-USER", "ACL2"), 103176998Sphk("BRR", "ACL2-USER", "ACL2"), 104176998Sphk("BRR@", "ACL2-USER", "ACL2"), 105176998Sphk("BUILD-STATE1", "ACL2-USER", "ACL2"), 106176998Sphk("CAR-CDR-ELIM", "ACL2-USER", "ACL2"), 107176998Sphk("CAR-CONS", "ACL2-USER", "ACL2"), 108176998Sphk("CASE-LIST", "ACL2-USER", "ACL2"), 109219095Sphk("CASE-LIST-CHECK", "ACL2-USER", "ACL2"), 110176998Sphk("CASE-MATCH", "ACL2-USER", "ACL2"), 111219095Sphk("CASE-SPLIT", "ACL2-USER", "ACL2"), 112176998Sphk("CASE-TEST", "ACL2-USER", "ACL2"), 113219095Sphk("CBD", "ACL2-USER", "ACL2"), 114176998Sphk("CDR-CONS", "ACL2-USER", "ACL2"), 115176998Sphk("CDRN", "ACL2-USER", "ACL2"), 116("CERTIFY-BOOK", "ACL2-USER", "ACL2"), 117("CERTIFY-BOOK!", "ACL2-USER", "ACL2"), 118("CHAR-CODE-CODE-CHAR-IS-IDENTITY", "ACL2-USER", "ACL2"), 119("CHAR-CODE-LINEAR", "ACL2-USER", "ACL2"), 120("CHARACTER-LISTP", "ACL2-USER", "ACL2"), 121("CHARACTER-LISTP-APPEND", "ACL2-USER", "ACL2"), 122("CHARACTER-LISTP-COERCE", "ACL2-USER", "ACL2"), 123("CHARACTER-LISTP-FORWARD-TO-EQLABLE-LISTP", "ACL2-USER", "ACL2"), 124("CHARACTER-LISTP-REMOVE-DUPLICATES-EQL", "ACL2-USER", "ACL2"), 125("CHARACTER-LISTP-REVAPPEND", "ACL2-USER", "ACL2"), 126("CHARACTER-LISTP-STRING-DOWNCASE-1", "ACL2-USER", "ACL2"), 127("CHARACTER-LISTP-STRING-UPCASE1-1", "ACL2-USER", "ACL2"), 128("CHARACTERP-CHAR-DOWNCASE", "ACL2-USER", "ACL2"), 129("CHARACTERP-CHAR-UPCASE", "ACL2-USER", "ACL2"), 130("CHARACTERP-NTH", "ACL2-USER", "ACL2"), 131("CHARACTERP-PAGE", "ACL2-USER", "ACL2"), 132("CHARACTERP-RUBOUT", "ACL2-USER", "ACL2"), 133("CHARACTERP-TAB", "ACL2-USER", "ACL2"), 134("CHECK-VARS-NOT-FREE", "ACL2-USER", "ACL2"), 135("CHECKPOINT-FORCED-GOALS", "ACL2-USER", "ACL2"), 136("CLAUSE", "ACL2-USER", "ACL2"), 137("CLOSE-INPUT-CHANNEL", "ACL2-USER", "ACL2"), 138("CLOSE-OUTPUT-CHANNEL", "ACL2-USER", "ACL2"), 139("CLOSURE", "ACL2-USER", "ACL2"), 140("CODE-CHAR-CHAR-CODE-IS-IDENTITY", "ACL2-USER", "ACL2"), 141("CODE-CHAR-TYPE", "ACL2-USER", "ACL2"), 142("COERCE-INVERSE-1", "ACL2-USER", "ACL2"), 143("COERCE-INVERSE-2", "ACL2-USER", "ACL2"), 144("COERCE-OBJECT-TO-STATE", "ACL2-USER", "ACL2"), 145("COERCE-STATE-TO-OBJECT", "ACL2-USER", "ACL2"), 146("COMMUTATIVITY-OF-*", "ACL2-USER", "ACL2"), 147("COMMUTATIVITY-OF-+", "ACL2-USER", "ACL2"), 148("COMP", "ACL2-USER", "ACL2"), 149("COMPLETION-OF-*", "ACL2-USER", "ACL2"), 150("COMPLETION-OF-+", "ACL2-USER", "ACL2"), 151("COMPLETION-OF-<", "ACL2-USER", "ACL2"), 152("COMPLETION-OF-CAR", "ACL2-USER", "ACL2"), 153("COMPLETION-OF-CDR", "ACL2-USER", "ACL2"), 154("COMPLETION-OF-CHAR-CODE", "ACL2-USER", "ACL2"), 155("COMPLETION-OF-CODE-CHAR", "ACL2-USER", "ACL2"), 156("COMPLETION-OF-COERCE", "ACL2-USER", "ACL2"), 157("COMPLETION-OF-COMPLEX", "ACL2-USER", "ACL2"), 158("COMPLETION-OF-DENOMINATOR", "ACL2-USER", "ACL2"), 159("COMPLETION-OF-IMAGPART", "ACL2-USER", "ACL2"), 160("COMPLETION-OF-INTERN-IN-PACKAGE-OF-SYMBOL", "ACL2-USER", "ACL2"), 161("COMPLETION-OF-NUMERATOR", "ACL2-USER", "ACL2"), 162("COMPLETION-OF-REALPART", "ACL2-USER", "ACL2"), 163("COMPLETION-OF-SYMBOL-NAME", "ACL2-USER", "ACL2"), 164("COMPLETION-OF-SYMBOL-PACKAGE-NAME", "ACL2-USER", "ACL2"), 165("COMPLETION-OF-UNARY-/", "ACL2-USER", "ACL2"), 166("COMPLETION-OF-UNARY-MINUS", "ACL2-USER", "ACL2"), 167("COMPLEX-0", "ACL2-USER", "ACL2"), 168("COMPLEX-DEFINITION", "ACL2-USER", "ACL2"), 169("COMPLEX-EQUAL", "ACL2-USER", "ACL2"), 170("COMPLEX-IMPLIES1", "ACL2-USER", "ACL2"), 171("COMPLEX-RATIONALP", "ACL2-USER", "ACL2"), 172("COMPRESS1", "ACL2-USER", "ACL2"), 173("COMPRESS11", "ACL2-USER", "ACL2"), 174("COMPRESS2", "ACL2-USER", "ACL2"), 175("COMPRESS21", "ACL2-USER", "ACL2"), 176("COMPRESS211", "ACL2-USER", "ACL2"), 177("COND-CLAUSESP", "ACL2-USER", "ACL2"), 178("COND-MACRO", "ACL2-USER", "ACL2"), 179("CONS-EQUAL", "ACL2-USER", "ACL2"), 180("CONSP-ASSOC", "ACL2-USER", "ACL2"), 181("CONSP-ASSOC-EQ", "ACL2-USER", "ACL2"), 182("CURRENT-PACKAGE", "ACL2-USER", "ACL2"), 183("CURRENT-THEORY", "ACL2-USER", "ACL2"), 184("CW-GSTACK", "ACL2-USER", "ACL2"), 185("CW", "ACL2-USER", "ACL2"), 186("DECREMENT-BIG-CLOCK", "ACL2-USER", "ACL2"), 187("DEFABBREV", "ACL2-USER", "ACL2"), 188("DEFAULT", "ACL2-USER", "ACL2"), 189("DEFAULT-*-1", "ACL2-USER", "ACL2"), 190("DEFAULT-*-2", "ACL2-USER", "ACL2"), 191("DEFAULT-+-1", "ACL2-USER", "ACL2"), 192("DEFAULT-+-2", "ACL2-USER", "ACL2"), 193("DEFAULT-<-1", "ACL2-USER", "ACL2"), 194("DEFAULT-<-2", "ACL2-USER", "ACL2"), 195("DEFAULT-CAR", "ACL2-USER", "ACL2"), 196("DEFAULT-CDR", "ACL2-USER", "ACL2"), 197("DEFAULT-CHAR-CODE", "ACL2-USER", "ACL2"), 198("DEFAULT-COERCE-1", "ACL2-USER", "ACL2"), 199("DEFAULT-COERCE-2", "ACL2-USER", "ACL2"), 200("DEFAULT-COERCE-3", "ACL2-USER", "ACL2"), 201("DEFAULT-COMPILE-FNS", "ACL2-USER", "ACL2"), 202("DEFAULT-COMPLEX-1", "ACL2-USER", "ACL2"), 203("DEFAULT-COMPLEX-2", "ACL2-USER", "ACL2"), 204("DEFAULT-DEFUN-MODE", "ACL2-USER", "ACL2"), 205("DEFAULT-DEFUN-MODE-FROM-STATE", "ACL2-USER", "ACL2"), 206("DEFAULT-DENOMINATOR", "ACL2-USER", "ACL2"), 207("DEFAULT-IMAGPART", "ACL2-USER", "ACL2"), 208("DEFAULT-MEASURE-FUNCTION", "ACL2-USER", "ACL2"), 209("DEFAULT-NUMERATOR", "ACL2-USER", "ACL2"), 210("DEFAULT-REALPART", "ACL2-USER", "ACL2"), 211("DEFAULT-SYMBOL-NAME", "ACL2-USER", "ACL2"), 212("DEFAULT-SYMBOL-PACKAGE-NAME", "ACL2-USER", "ACL2"), 213("DEFAULT-UNARY-/", "ACL2-USER", "ACL2"), 214("DEFAULT-UNARY-MINUS", "ACL2-USER", "ACL2"), 215("DEFAULT-VERIFY-GUARDS-EAGERNESS", "ACL2-USER", "ACL2"), 216("DEFAULT-WELL-FOUNDED-RELATION", "ACL2-USER", "ACL2"), 217("DEFAXIOM", "ACL2-USER", "ACL2"), 218("DEFCHOOSE", "ACL2-USER", "ACL2"), 219("DEFCONG", "ACL2-USER", "ACL2"), 220("DEFCONST", "ACL2-USER", "ACL2"), 221("DEFDOC", "ACL2-USER", "ACL2"), 222("DEFEQUIV", "ACL2-USER", "ACL2"), 223("DEFEVALUATOR", "ACL2-USER", "ACL2"), 224("DEFEXEC", "ACL2-USER", "ACL2"), 225("DEFINE-PC-ATOMIC-MACRO", "ACL2-USER", "ACL2"), 226("DEFINE-PC-HELP", "ACL2-USER", "ACL2"), 227("DEFINE-PC-MACRO", "ACL2-USER", "ACL2"), 228("DEFLABEL", "ACL2-USER", "ACL2"), 229("DEFPKG", "ACL2-USER", "ACL2"), 230("DEFREFINEMENT", "ACL2-USER", "ACL2"), 231("DEFSTOBJ", "ACL2-USER", "ACL2"), 232("DEFSTUB", "ACL2-USER", "ACL2"), 233("DEFTHEORY", "ACL2-USER", "ACL2"), 234("DEFTHM", "ACL2-USER", "ACL2"), 235("DEFTHMD", "ACL2-USER", "ACL2"), 236("DEFUND", "ACL2-USER", "ACL2"), 237("DEFUN-SK", "ACL2-USER", "ACL2"), 238("DEFUNS", "ACL2-USER", "ACL2"), 239("DELETE-PAIR", "ACL2-USER", "ACL2"), 240("DIGIT-TO-CHAR", "ACL2-USER", "ACL2"), 241("DIMENSIONS", "ACL2-USER", "ACL2"), 242("DISABLE", "ACL2-USER", "ACL2"), 243("DISABLE-FORCING", "ACL2-USER", "ACL2"), 244("DISABLEDP", "ACL2-USER", "ACL2"), 245("DISTRIBUTIVITY", "ACL2-USER", "ACL2"), 246("DOC", "ACL2-USER", "ACL2"), 247("DOC!", "ACL2-USER", "ACL2"), 248("DOCS", "ACL2-USER", "ACL2"), 249("DUPLICATES", "ACL2-USER", "ACL2"), 250("E/D", "ACL2-USER", "ACL2"), 251("E0-ORD-<", "ACL2-USER", "ACL2"), 252("E0-ORDINALP", "ACL2-USER", "ACL2"), 253("ELIMINATE-DESTRUCTORS", "ACL2-USER", "ACL2"), 254("ELIMINATE-IRRELEVANCE", "ACL2-USER", "ACL2"), 255("ENABLE", "ACL2-USER", "ACL2"), 256("ENABLE-FORCING", "ACL2-USER", "ACL2"), 257("ENCAPSULATE", "ACL2-USER", "ACL2"), 258("EQLABLE-ALISTP", "ACL2-USER", "ACL2"), 259("EQLABLE-ALISTP-FORWARD-TO-ALISTP", "ACL2-USER", "ACL2"), 260("EQLABLE-LISTP", "ACL2-USER", "ACL2"), 261("EQLABLE-LISTP-FORWARD-TO-ATOM-LISTP", "ACL2-USER", "ACL2"), 262("EQLABLEP", "ACL2-USER", "ACL2"), 263("EQLABLEP-RECOG", "ACL2-USER", "ACL2"), 264("EQUAL-CHAR-CODE", "ACL2-USER", "ACL2"), 265("ER", "ACL2-USER", "ACL2"), 266("ER-PROGN", "ACL2-USER", "ACL2"), 267("ER-PROGN-FN", "ACL2-USER", "ACL2"), 268("EVENS", "ACL2-USER", "ACL2"), 269("EVENT", "ACL2-USER", "ACL2"), 270("EXECUTABLE-COUNTERPART-THEORY", "ACL2-USER", "ACL2"), 271("EXPLODE-ATOM", "ACL2-USER", "ACL2"), 272("EXPLODE-NONNEGATIVE-INTEGER", "ACL2-USER", "ACL2"), 273("EXPT-TYPE-PRESCRIPTION-NON-ZERO-BASE", "ACL2-USER", "ACL2"), 274("EXTEND-32-BIT-INTEGER-STACK", "ACL2-USER", "ACL2"), 275("EXTEND-T-STACK", "ACL2-USER", "ACL2"), 276("EXTEND-WORLD", "ACL2-USER", "ACL2"), 277("FERTILIZE", "ACL2-USER", "ACL2"), 278("FGETPROP", "ACL2-USER", "ACL2"), 279("FILE-CLOCK", "ACL2-USER", "ACL2"), 280("FILE-CLOCK-P", "ACL2-USER", "ACL2"), 281("FILE-CLOCK-P-FORWARD-TO-INTEGERP", "ACL2-USER", "ACL2"), 282("FIRST-N-AC", "ACL2-USER", "ACL2"), 283("FIX", "ACL2-USER", "ACL2"), 284("FIX-TRUE-LIST", "ACL2-USER", "ACL2"), 285("FMS", "ACL2-USER", "ACL2"), 286("FMT", "ACL2-USER", "ACL2"), 287("FMT-TO-COMMENT-WINDOW", "ACL2-USER", "ACL2"), 288("FMT1", "ACL2-USER", "ACL2"), 289("FORCE", "ACL2-USER", "ACL2"), 290("FUNCTION-SYMBOLP", "ACL2-USER", "ACL2"), 291("FUNCTION-THEORY", "ACL2-USER", "ACL2"), 292("GENERALIZE", "ACL2-USER", "ACL2"), 293("GET-GLOBAL", "ACL2-USER", "ACL2"), 294("GET-TIMER", "ACL2-USER", "ACL2"), 295("GETPROP-DEFAULT", "ACL2-USER", "ACL2"), 296("GETPROPS", "ACL2-USER", "ACL2"), 297("GETPROPS1", "ACL2-USER", "ACL2"), 298("GLOBAL-TABLE", "ACL2-USER", "ACL2"), 299("GLOBAL-TABLE-CARS", "ACL2-USER", "ACL2"), 300("GLOBAL-TABLE-CARS1", "ACL2-USER", "ACL2"), 301("GLOBAL-VAL", "ACL2-USER", "ACL2"), 302("GOOD-BYE", "ACL2-USER", "ACL2"), 303("GOOD-DEFUN-MODE-P", "ACL2-USER", "ACL2"), 304("GROUND-ZERO", "ACL2-USER", "ACL2"), 305("HARD-ERROR", "ACL2-USER", "ACL2"), 306("HAS-PROPSP", "ACL2-USER", "ACL2"), 307("HAS-PROPSP1", "ACL2-USER", "ACL2"), 308("HEADER", "ACL2-USER", "ACL2"), 309("HELP", "ACL2-USER", "ACL2"), 310("HIDE", "ACL2-USER", "ACL2"), 311("I-AM-HERE", "ACL2-USER", "ACL2"), 312("ID", "ACL2-USER", "ACL2"), 313("IDATES", "ACL2-USER", "ACL2"), 314("IF*", "ACL2-USER", "ACL2"), 315("IFF", "ACL2-USER", "ACL2"), 316("IFF-IMPLIES-EQUAL-IMPLIES-1", "ACL2-USER", "ACL2"), 317("IFF-IMPLIES-EQUAL-IMPLIES-2", "ACL2-USER", "ACL2"), 318("IFF-IMPLIES-EQUAL-NOT", "ACL2-USER", "ACL2"), 319("IFF-IS-AN-EQUIVALENCE", "ACL2-USER", "ACL2"), 320("IFIX", "ACL2-USER", "ACL2"), 321("ILLEGAL", "ACL2-USER", "ACL2"), 322("IMAGPART-COMPLEX", "ACL2-USER", "ACL2"), 323("IMMEDIATE-FORCE-MODEP", "ACL2-USER", "ACL2"), 324("IMPLIES", "ACL2-USER", "ACL2"), 325("IMPROPER-CONSP", "ACL2-USER", "ACL2"), 326("IN-THEORY", "ACL2-USER", "ACL2"), 327("IN-ARITHMETIC-THEORY", "ACL2-USER", "ACL2"), 328("INCLUDE-BOOK", "ACL2-USER", "ACL2"), 329("INCOMPATIBLE", "ACL2-USER", "ACL2"), 330("INCREMENT-TIMER", "ACL2-USER", "ACL2"), 331("INDUCT", "ACL2-USER", "ACL2"), 332("INT=", "ACL2-USER", "ACL2"), 333("INTEGER-0", "ACL2-USER", "ACL2"), 334("INTEGER-1", "ACL2-USER", "ACL2"), 335("INTEGER-ABS", "ACL2-USER", "ACL2"), 336("INTEGER-IMPLIES-RATIONAL", "ACL2-USER", "ACL2"), 337("INTEGER-LISTP", "ACL2-USER", "ACL2"), 338("INTEGER-LISTP-FORWARD-TO-RATIONAL-LISTP", "ACL2-USER", "ACL2"), 339("INTEGER-STEP", "ACL2-USER", "ACL2"), 340("INTERN$", "ACL2-USER", "ACL2"), 341("INTERN-IN-PACKAGE-OF-SYMBOL", "ACL2-USER", "ACL2"), 342("INTERN-IN-PACKAGE-OF-SYMBOL-SYMBOL-NAME", "ACL2-USER", "ACL2"), 343("INTERSECTION-EQ", "ACL2-USER", "ACL2"), 344("INTERSECTION-THEORIES", "ACL2-USER", "ACL2"), 345("INTERSECTP-EQ", "ACL2-USER", "ACL2"), 346("INTERSECTP-EQUAL", "ACL2-USER", "ACL2"), 347("INVERSE-OF-*", "ACL2-USER", "ACL2"), 348("INVERSE-OF-+", "ACL2-USER", "ACL2"), 349("INVISIBLE-FNS-TABLE", "ACL2-USER", "ACL2"), 350("KEYWORD-PACKAGE", "ACL2-USER", "ACL2"), 351("KEYWORD-VALUE-LISTP", "ACL2-USER", "ACL2"), 352("KEYWORD-VALUE-LISTP-ASSOC-KEYWORD", "ACL2-USER", "ACL2"), 353("KEYWORD-VALUE-LISTP-FORWARD-TO-TRUE-LISTP", "ACL2-USER", "ACL2"), 354("KEYWORDP-FORWARD-TO-SYMBOLP", "ACL2-USER", "ACL2"), 355("KNOWN-PACKAGE-ALIST", "ACL2-USER", "ACL2"), 356("KNOWN-PACKAGE-ALISTP", "ACL2-USER", "ACL2"), 357("KNOWN-PACKAGE-ALISTP-FORWARD-TO-TRUE-LIST-LISTP-AND-ALISTP", "ACL2-USER", 358"ACL2"), 359("LD", "ACL2-USER", "ACL2"), 360("LD-ERROR-ACTION", "ACL2-USER", "ACL2"), 361("LD-ERROR-TRIPLES", "ACL2-USER", "ACL2"), 362("LD-KEYWORD-ALIASES", "ACL2-USER", "ACL2"), 363("LD-POST-EVAL-PRINT", "ACL2-USER", "ACL2"), 364("LD-PRE-EVAL-FILTER", "ACL2-USER", "ACL2"), 365("LD-PRE-EVAL-PRINT", "ACL2-USER", "ACL2"), 366("LD-PROMPT", "ACL2-USER", "ACL2"), 367("LD-QUERY-CONTROL-ALIST", "ACL2-USER", "ACL2"), 368("LD-REDEFINITION-ACTION", "ACL2-USER", "ACL2"), 369("LD-SKIP-PROOFSP", "ACL2-USER", "ACL2"), 370("LD-VERBOSE", "ACL2-USER", "ACL2"), 371("LEGAL-CASE-CLAUSESP", "ACL2-USER", "ACL2"), 372("LEN", "ACL2-USER", "ACL2"), 373("LEN-UPDATE-NTH", "ACL2-USER", "ACL2"), 374("LIST*-MACRO", "ACL2-USER", "ACL2"), 375("LIST-ALL-PACKAGE-NAMES", "ACL2-USER", "ACL2"), 376("LIST-ALL-PACKAGE-NAMES-LST", "ACL2-USER", "ACL2"), 377("LIST-MACRO", "ACL2-USER", "ACL2"), 378("LOCAL", "ACL2-USER", "ACL2"), 379("LOGIC", "ACL2-USER", "ACL2"), 380("LOWER-CASE-P-CHAR-DOWNCASE", "ACL2-USER", "ACL2"), 381("LOWER-CASE-P-FORWARD-TO-ALPHA-CHAR-P", "ACL2-USER", "ACL2"), 382("LOWEST-TERMS", "ACL2-USER", "ACL2"), 383("LP", "ACL2-USER", "ACL2"), 384("MACRO-ALIASES", "ACL2-USER", "ACL2"), 385("NTH-ALIASES", "ACL2-USER", "ACL2"), 386("MAIN-TIMER", "ACL2-USER", "ACL2"), 387("MAIN-TIMER-TYPE-PRESCRIPTION", "ACL2-USER", "ACL2"), 388("MAKE-CHARACTER-LIST", "ACL2-USER", "ACL2"), 389("MAKE-CHARACTER-LIST-MAKE-CHARACTER-LIST", "ACL2-USER", "ACL2"), 390("MAKE-FMT-BINDINGS", "ACL2-USER", "ACL2"), 391("MAKE-INPUT-CHANNEL", "ACL2-USER", "ACL2"), 392("MAKE-LIST-AC", "ACL2-USER", "ACL2"), 393("MAKE-MV-NTHS", "ACL2-USER", "ACL2"), 394("MAKE-ORD", "ACL2-USER", "ACL2"), 395("MAKE-OUTPUT-CHANNEL", "ACL2-USER", "ACL2"), 396("MAKE-VAR-LST", "ACL2-USER", "ACL2"), 397("MAKE-VAR-LST1", "ACL2-USER", "ACL2"), 398("MAKUNBOUND-GLOBAL", "ACL2-USER", "ACL2"), 399("MAXIMUM-LENGTH", "ACL2-USER", "ACL2"), 400("MAY-NEED-SLASHES", "ACL2-USER", "ACL2"), 401("MBE", "ACL2-USER", "ACL2"), 402("MBT", "ACL2-USER", "ACL2"), 403("MEMBER-EQ", "ACL2-USER", "ACL2"), 404("MEMBER-EQUAL", "ACL2-USER", "ACL2"), 405("MEMBER-SYMBOL-NAME", "ACL2-USER", "ACL2"), 406("MFC", "ACL2-USER", "ACL2"), 407("MINIMAL-THEORY", "ACL2-USER", "ACL2"), 408("MONITOR", "ACL2-USER", "ACL2"), 409("MONITORED-RUNES", "ACL2-USER", "ACL2"), 410("MORE", "ACL2-USER", "ACL2"), 411("MORE!", "ACL2-USER", "ACL2"), 412("MORE-DOC", "ACL2-USER", "ACL2"), 413("MUTUAL-RECURSION", "ACL2-USER", "ACL2"), 414("MUTUAL-RECURSION-GUARDP", "ACL2-USER", "ACL2"), 415("MV", "ACL2-USER", "ACL2"), 416("MV-LET", "ACL2-USER", "ACL2"), 417("MV-NTH", "ACL2-USER", "ACL2"), 418("NATP", "ACL2-USER", "ACL2"), 419("NEWLINE", "ACL2-USER", "ACL2"), 420("NFIX", "ACL2-USER", "ACL2"), 421("NIL-IS-NOT-CIRCULAR", "ACL2-USER", "ACL2"), 422("NO-DUPLICATESP", "ACL2-USER", "ACL2"), 423("NO-DUPLICATESP-EQUAL", "ACL2-USER", "ACL2"), 424("NONNEGATIVE-INTEGER-QUOTIENT", "ACL2-USER", "ACL2"), 425("NONNEGATIVE-PRODUCT", "ACL2-USER", "ACL2"), 426("NONZERO-IMAGPART", "ACL2-USER", "ACL2"), 427("NQTHM-TO-ACL2", "ACL2-USER", "ACL2"), 428("NTH-0-CONS", "ACL2-USER", "ACL2"), 429("NTH-0-READ-RUN-TIME-TYPE-PRESCRIPTION", "ACL2-USER", "ACL2"), 430("NTH-ADD1", "ACL2-USER", "ACL2"), 431("NTH-UPDATE-NTH", "ACL2-USER", "ACL2"), 432("O<", "ACL2-USER", "ACL2"), 433("O<=", "ACL2-USER", "ACL2"), 434("O>", "ACL2-USER", "ACL2"), 435("O>=", "ACL2-USER", "ACL2"), 436("O-FINP", "ACL2-USER", "ACL2"), 437("O-FIRST-COEFF", "ACL2-USER", "ACL2"), 438("O-FIRST-EXPT", "ACL2-USER", "ACL2"), 439("O-INFP", "ACL2-USER", "ACL2"), 440("O-P", "ACL2-USER", "ACL2"), 441("O-RST", "ACL2-USER", "ACL2"), 442("OBSERVATION", "ACL2-USER", "ACL2"), 443("ODDS", "ACL2-USER", "ACL2"), 444("OK-IF", "ACL2-USER", "ACL2"), 445("OOPS", "ACL2-USER", "ACL2"), 446("OPEN-CHANNEL-LISTP", "ACL2-USER", "ACL2"), 447("OPEN-CHANNEL1", "ACL2-USER", "ACL2"), 448("OPEN-CHANNEL1-FORWARD-TO-TRUE-LISTP-AND-CONSP", "ACL2-USER", "ACL2"), 449("OPEN-CHANNELS-P", "ACL2-USER", "ACL2"), 450("OPEN-CHANNELS-P-FORWARD", "ACL2-USER", "ACL2"), 451("OPEN-INPUT-CHANNEL", "ACL2-USER", "ACL2"), 452("OPEN-INPUT-CHANNEL-ANY-P", "ACL2-USER", "ACL2"), 453("OPEN-INPUT-CHANNEL-ANY-P1", "ACL2-USER", "ACL2"), 454("OPEN-INPUT-CHANNEL-P", "ACL2-USER", "ACL2"), 455("OPEN-INPUT-CHANNEL-P1", "ACL2-USER", "ACL2"), 456("OPEN-INPUT-CHANNELS", "ACL2-USER", "ACL2"), 457("OPEN-OUTPUT-CHANNEL", "ACL2-USER", "ACL2"), 458("OPEN-OUTPUT-CHANNEL-ANY-P", "ACL2-USER", "ACL2"), 459("OPEN-OUTPUT-CHANNEL-ANY-P1", "ACL2-USER", "ACL2"), 460("OPEN-OUTPUT-CHANNEL-P", "ACL2-USER", "ACL2"), 461("OPEN-OUTPUT-CHANNEL-P1", "ACL2-USER", "ACL2"), 462("OPEN-OUTPUT-CHANNELS", "ACL2-USER", "ACL2"), 463("OR-MACRO", "ACL2-USER", "ACL2"), 464("ORDERED-SYMBOL-ALISTP", "ACL2-USER", "ACL2"), 465("ORDERED-SYMBOL-ALISTP-ADD-PAIR", "ACL2-USER", "ACL2"), 466("ORDERED-SYMBOL-ALISTP-ADD-PAIR-FORWARD", "ACL2-USER", "ACL2"), 467("ORDERED-SYMBOL-ALISTP-FORWARD-TO-SYMBOL-ALISTP", "ACL2-USER", "ACL2"), 468("ORDERED-SYMBOL-ALISTP-GETPROPS", "ACL2-USER", "ACL2"), 469("ORDERED-SYMBOL-ALISTP-REMOVE-FIRST-PAIR", "ACL2-USER", "ACL2"), 470("OUR-DIGIT-CHAR-P", "ACL2-USER", "ACL2"), 471("PAIRLIS$", "ACL2-USER", "ACL2"), 472("PAIRLIS2", "ACL2-USER", "ACL2"), 473("PBT", "ACL2-USER", "ACL2"), 474("PC", "ACL2-USER", "ACL2"), 475("PCB", "ACL2-USER", "ACL2"), 476("PCB!", "ACL2-USER", "ACL2"), 477("PCS", "ACL2-USER", "ACL2"), 478("PE", "ACL2-USER", "ACL2"), 479("PE!", "ACL2-USER", "ACL2"), 480("PEEK-CHAR$", "ACL2-USER", "ACL2"), 481("PF", "ACL2-USER", "ACL2"), 482("PL", "ACL2-USER", "ACL2"), 483("POP-TIMER", "ACL2-USER", "ACL2"), 484("POSITION-AC", "ACL2-USER", "ACL2"), 485("POSITION-EQ", "ACL2-USER", "ACL2"), 486("POSITION-EQ-AC", "ACL2-USER", "ACL2"), 487("POSITION-EQUAL", "ACL2-USER", "ACL2"), 488("POSITION-EQUAL-AC", "ACL2-USER", "ACL2"), 489("POSITIVE", "ACL2-USER", "ACL2"), 490("POSP", "ACL2-USER", "ACL2"), 491("POWER-EVAL", "ACL2-USER", "ACL2"), 492("PPROGN", "ACL2-USER", "ACL2"), 493("PR", "ACL2-USER", "ACL2"), 494("PR!", "ACL2-USER", "ACL2"), 495("PREPROCESS", "ACL2-USER", "ACL2"), 496("PRIN1$", "ACL2-USER", "ACL2"), 497("PRIN1-WITH-SLASHES", "ACL2-USER", "ACL2"), 498("PRIN1-WITH-SLASHES1", "ACL2-USER", "ACL2"), 499("PRINC$", "ACL2-USER", "ACL2"), 500("PRINT-OBJECT$", "ACL2-USER", "ACL2"), 501("PRINT-RATIONAL-AS-DECIMAL", "ACL2-USER", "ACL2"), 502("PRINT-TIMER", "ACL2-USER", "ACL2"), 503("PROG2$", "ACL2-USER", "ACL2"), 504("PROGRAM", "ACL2-USER", "ACL2"), 505("PROOF-TREE", "ACL2-USER", "ACL2"), 506("PROOFS-CO", "ACL2-USER", "ACL2"), 507("PROPER-CONSP", "ACL2-USER", "ACL2"), 508("PROPS", "ACL2-USER", "ACL2"), 509("PROVE", "ACL2-USER", "ACL2"), 510("PSEUDO-TERM-LISTP", "ACL2-USER", "ACL2"), 511("PSEUDO-TERM-LISTP-FORWARD-TO-TRUE-LISTP", "ACL2-USER", "ACL2"), 512("PSEUDO-TERMP", "ACL2-USER", "ACL2"), 513("PSTACK", "ACL2-USER", "ACL2"), 514("PUFF", "ACL2-USER", "ACL2"), 515("PUFF*", "ACL2-USER", "ACL2"), 516("PUSH-TIMER", "ACL2-USER", "ACL2"), 517("PUSH-UNTOUCHABLE", "ACL2-USER", "ACL2"), 518("PUT-ASSOC-EQ", "ACL2-USER", "ACL2"), 519("PUT-ASSOC-EQUAL", "ACL2-USER", "ACL2"), 520("PUT-GLOBAL", "ACL2-USER", "ACL2"), 521("PUTPROP", "ACL2-USER", "ACL2"), 522("QUOTEP", "ACL2-USER", "ACL2"), 523("R-EQLABLE-ALISTP", "ACL2-USER", "ACL2"), 524("RASSOC-EQ", "ACL2-USER", "ACL2"), 525("RASSOC-EQUAL", "ACL2-USER", "ACL2"), 526("RATIONAL-IMPLIES1", "ACL2-USER", "ACL2"), 527("RATIONAL-IMPLIES2", "ACL2-USER", "ACL2"), 528("RATIONAL-LISTP", "ACL2-USER", "ACL2"), 529("RATIONAL-LISTP-FORWARD-TO-TRUE-LISTP", "ACL2-USER", "ACL2"), 530("RATIONALP-*", "ACL2-USER", "ACL2"), 531("RATIONALP-+", "ACL2-USER", "ACL2"), 532("RATIONALP-EXPT-TYPE-PRESCRIPTION", "ACL2-USER", "ACL2"), 533("RATIONALP-IMPLIES-ACL2-NUMBERP", "ACL2-USER", "ACL2"), 534("RATIONALP-UNARY--", "ACL2-USER", "ACL2"), 535("RATIONALP-UNARY-/", "ACL2-USER", "ACL2"), 536("READ-BYTE$", "ACL2-USER", "ACL2"), 537("READ-CHAR$", "ACL2-USER", "ACL2"), 538("READ-FILE-LISTP", "ACL2-USER", "ACL2"), 539("READ-FILE-LISTP-FORWARD-TO-TRUE-LIST-LISTP", "ACL2-USER", "ACL2"), 540("READ-FILE-LISTP1", "ACL2-USER", "ACL2"), 541("READ-FILE-LISTP1-FORWARD-TO-TRUE-LISTP-AND-CONSP", "ACL2-USER", "ACL2"), 542("READ-FILES", "ACL2-USER", "ACL2"), 543("READ-FILES-P", "ACL2-USER", "ACL2"), 544("READ-FILES-P-FORWARD-TO-READ-FILE-LISTP", "ACL2-USER", "ACL2"), 545("READ-IDATE", "ACL2-USER", "ACL2"), 546("READ-OBJECT", "ACL2-USER", "ACL2"), 547("READ-RUN-TIME", "ACL2-USER", "ACL2"), 548("READ-RUN-TIME-PRESERVES-STATE-P1", "ACL2-USER", "ACL2"), 549("READABLE-FILE", "ACL2-USER", "ACL2"), 550("READABLE-FILE-FORWARD-TO-TRUE-LISTP-AND-CONSP", "ACL2-USER", "ACL2"), 551("READABLE-FILES", "ACL2-USER", "ACL2"), 552("READABLE-FILES-LISTP", "ACL2-USER", "ACL2"), 553("READABLE-FILES-LISTP-FORWARD-TO-TRUE-LIST-LISTP-AND-ALISTP", "ACL2-USER", 554"ACL2"), 555("READABLE-FILES-P", "ACL2-USER", "ACL2"), 556("READABLE-FILES-P-FORWARD-TO-READABLE-FILES-LISTP", "ACL2-USER", "ACL2"), 557("REAL/RATIONALP", "ACL2-USER", "ACL2"), 558("REALFIX", "ACL2-USER", "ACL2"), 559("REALPART-COMPLEX", "ACL2-USER", "ACL2"), 560("REALPART-IMAGPART-ELIM", "ACL2-USER", "ACL2"), 561("REBUILD", "ACL2-USER", "ACL2"), 562("REDEF", "ACL2-USER", "ACL2"), 563("REDEF!", "ACL2-USER", "ACL2"), 564("REMOVE-DEFAULT-HINTS", "ACL2-USER", "ACL2"), 565("REMOVE-DEFAULT-HINTS!", "ACL2-USER", "ACL2"), 566("REMOVE-DUPLICATES-EQL", "ACL2-USER", "ACL2"), 567("REMOVE-DUPLICATES-EQUAL", "ACL2-USER", "ACL2"), 568("REMOVE-FIRST-PAIR", "ACL2-USER", "ACL2"), 569("REMOVE-MACRO-ALIAS", "ACL2-USER", "ACL2"), 570("REMOVE-NTH-ALIAS", "ACL2-USER", "ACL2"), 571("RESET-LD-SPECIALS", "ACL2-USER", "ACL2"), 572("RETRACT-WORLD", "ACL2-USER", "ACL2"), 573("RETRIEVE", "ACL2-USER", "ACL2"), 574("RFIX", "ACL2-USER", "ACL2"), 575("RUN-TIMES", "ACL2-USER", "ACL2"), 576("SET-BOGUS-MUTUAL-RECURSION-OK", "ACL2-USER", "ACL2"), 577("SET-CBD", "ACL2-USER", "ACL2"), 578("SET-CASE-SPLIT-LIMITATIONS", "ACL2-USER", "ACL2"), 579("SET-COMPILE-FNS", "ACL2-USER", "ACL2"), 580("SET-DEFAULT-HINTS", "ACL2-USER", "ACL2"), 581("SET-DEFAULT-HINTS!", "ACL2-USER", "ACL2"), 582("SET-DIFFERENCE-EQ", "ACL2-USER", "ACL2"), 583("SET-DIFFERENCE-EQUAL", "ACL2-USER", "ACL2"), 584("SET-DIFFERENCE-THEORIES", "ACL2-USER", "ACL2"), 585("SET-ENFORCE-REDUNDANCY", "ACL2-USER", "ACL2"), 586("SET-EQUALP-EQUAL", "ACL2-USER", "ACL2"), 587("SET-GUARD-CHECKING", "ACL2-USER", "ACL2"), 588("SET-IGNORE-OK", "ACL2-USER", "ACL2"), 589("SET-INHIBIT-OUTPUT-LST", "ACL2-USER", "ACL2"), 590("SET-INHIBIT-WARNINGS", "ACL2-USER", "ACL2"), 591("SET-INVISIBLE-FNS-TABLE", "ACL2-USER", "ACL2"), 592("SET-IRRELEVANT-FORMALS-OK", "ACL2-USER", "ACL2"), 593("SET-MEASURE-FUNCTION", "ACL2-USER", "ACL2"), 594("SET-NON-LINEARP", "ACL2-USER", "ACL2"), 595("SET-STATE-OK", "ACL2-USER", "ACL2"), 596("SET-TIMER", "ACL2-USER", "ACL2"), 597("SET-VERIFY-GUARDS-EAGERNESS", "ACL2-USER", "ACL2"), 598("SET-W", "ACL2-USER", "ACL2"), 599("SET-WELL-FOUNDED-RELATION", "ACL2-USER", "ACL2"), 600("SGETPROP", "ACL2-USER", "ACL2"), 601("SHOW-BDD", "ACL2-USER", "ACL2"), 602("SHOW-ACCUMULATED-PERSISTENCE", "ACL2-USER", "ACL2"), 603("SHRINK-32-BIT-INTEGER-STACK", "ACL2-USER", "ACL2"), 604("SHRINK-T-STACK", "ACL2-USER", "ACL2"), 605("SIMPLIFY", "ACL2-USER", "ACL2"), 606("SKIP-PROOFS", "ACL2-USER", "ACL2"), 607("SOME-SLASHABLE", "ACL2-USER", "ACL2"), 608("STABLE-UNDER-SIMPLIFICATIONP", "ACL2-USER", "ACL2"), 609("STANDARD-CHAR-LISTP", "ACL2-USER", "ACL2"), 610("STANDARD-CHAR-LISTP-APPEND", "ACL2-USER", "ACL2"), 611("STANDARD-CHAR-LISTP-FORWARD-TO-CHARACTER-LISTP", "ACL2-USER", "ACL2"), 612("STANDARD-CHAR-P-NTH", "ACL2-USER", "ACL2"), 613("STANDARD-CO", "ACL2-USER", "ACL2"), 614("STANDARD-OI", "ACL2-USER", "ACL2"), 615("START-PROOF-TREE", "ACL2-USER", "ACL2"), 616("STATE", "ACL2-USER", "ACL2"), 617("STATE-GLOBAL-LET*-CLEANUP", "ACL2-USER", "ACL2"), 618("STATE-GLOBAL-LET*-GET-GLOBALS", "ACL2-USER", "ACL2"), 619("STATE-GLOBAL-LET*-PUT-GLOBALS", "ACL2-USER", "ACL2"), 620("STATE-P", "ACL2-USER", "ACL2"), 621("STATE-P-IMPLIES-AND-FORWARD-TO-STATE-P1", "ACL2-USER", "ACL2"), 622("STATE-P1", "ACL2-USER", "ACL2"), 623("STATE-P1-FORWARD", "ACL2-USER", "ACL2"), 624("STATE-P1-UPDATE-MAIN-TIMER", "ACL2-USER", "ACL2"), 625("STATE-P1-UPDATE-NTH-2-WORLD", "ACL2-USER", "ACL2"), 626("STOP-PROOF-TREE", "ACL2-USER", "ACL2"), 627("STANDARD-STRING-ALISTP", "ACL2-USER", "ACL2"), 628("STANDARD-STRING-ALISTP-FORWARD-TO-ALISTP", "ACL2-USER", "ACL2"), 629("STRING-APPEND", "ACL2-USER", "ACL2"), 630("STRING-APPEND-LST", "ACL2-USER", "ACL2"), 631("STRING-DOWNCASE1", "ACL2-USER", "ACL2"), 632("STRING-EQUAL1", "ACL2-USER", "ACL2"), 633("STRING-IS-NOT-CIRCULAR", "ACL2-USER", "ACL2"), 634("STRING-LISTP", "ACL2-USER", "ACL2"), 635("STRING-UPCASE1", "ACL2-USER", "ACL2"), 636("STRING<-IRREFLEXIVE", "ACL2-USER", "ACL2"), 637("STRING<-L", "ACL2-USER", "ACL2"), 638("STRING<-L-ASYMMETRIC", "ACL2-USER", "ACL2"), 639("STRING<-L-IRREFLEXIVE", "ACL2-USER", "ACL2"), 640("STRING<-L-TRANSITIVE", "ACL2-USER", "ACL2"), 641("STRING<-L-TRICHOTOMY", "ACL2-USER", "ACL2"), 642("STRINGP-SYMBOL-PACKAGE-NAME", "ACL2-USER", "ACL2"), 643("STRIP-CARS", "ACL2-USER", "ACL2"), 644("STRIP-CDRS", "ACL2-USER", "ACL2"), 645("SUBSEQ-LIST", "ACL2-USER", "ACL2"), 646("SUBSETP-EQUAL", "ACL2-USER", "ACL2"), 647("SUBSTITUTE-AC", "ACL2-USER", "ACL2"), 648("SUMMARY", "ACL2-USER", "ACL2"), 649("SYMBOL-<", "ACL2-USER", "ACL2"), 650("SYMBOL-<-ASYMMETRIC", "ACL2-USER", "ACL2"), 651("SYMBOL-<-IRREFLEXIVE", "ACL2-USER", "ACL2"), 652("SYMBOL-<-TRANSITIVE", "ACL2-USER", "ACL2"), 653("SYMBOL-<-TRICHOTOMY", "ACL2-USER", "ACL2"), 654("SYMBOL-ALISTP", "ACL2-USER", "ACL2"), 655("SYMBOL-ALISTP-FORWARD-TO-EQLABLE-ALISTP", "ACL2-USER", "ACL2"), 656("SYMBOL-DOUBLET-LISTP", "ACL2-USER", "ACL2"), 657("SYMBOL-EQUALITY", "ACL2-USER", "ACL2"), 658("SYMBOL-LISTP", "ACL2-USER", "ACL2"), 659("SYMBOL-LISTP-FORWARD-TO-TRUE-LISTP", "ACL2-USER", "ACL2"), 660("SYMBOL-NAME-INTERN-IN-PACKAGE-OF-SYMBOL", "ACL2-USER", "ACL2"), 661("SYMBOL-PACKAGE-NAME", "ACL2-USER", "ACL2"), 662("SYMBOLP-INTERN-IN-PACKAGE-OF-SYMBOL", "ACL2-USER", "ACL2"), 663("SYNP", "ACL2-USER", "ACL2"), 664("SYNTAXP", "ACL2-USER", "ACL2"), 665("SYS-CALL", "ACL2-USER", "ACL2"), 666("SYS-CALL-STATUS", "ACL2-USER", "ACL2"), 667("T-STACK", "ACL2-USER", "ACL2"), 668("T-STACK-LENGTH", "ACL2-USER", "ACL2"), 669("T-STACK-LENGTH1", "ACL2-USER", "ACL2"), 670("TABLE", "ACL2-USER", "ACL2"), 671("TABLE-ALIST", "ACL2-USER", "ACL2"), 672("TAKE", "ACL2-USER", "ACL2"), 673("THE-ERROR", "ACL2-USER", "ACL2"), 674("THE-FIXNUM", "ACL2-USER", "ACL2"), 675("THE-FIXNUM!", "ACL2-USER", "ACL2"), 676("THEORY", "ACL2-USER", "ACL2"), 677("THEORY-INVARIANT", "ACL2-USER", "ACL2"), 678("THM", "ACL2-USER", "ACL2"), 679("TIMER-ALISTP", "ACL2-USER", "ACL2"), 680("TIMER-ALISTP-FORWARD-TO-TRUE-LIST-LISTP-AND-SYMBOL-ALISTP", "ACL2-USER", 681"ACL2"), 682("TOGGLE-PC-MACRO", "ACL2-USER", "ACL2"), 683("TRACE$", "ACL2-USER", "ACL2"), 684("TRANS", "ACL2-USER", "ACL2"), 685("TRANS1", "ACL2-USER", "ACL2"), 686("TRICHOTOMY", "ACL2-USER", "ACL2"), 687("TRUE-LISTP", "ACL2-USER", "ACL2"), 688("TRUE-LIST-LISTP", "ACL2-USER", "ACL2"), 689("TRUE-LIST-LISTP-FORWARD-TO-TRUE-LISTP", "ACL2-USER", "ACL2"), 690("TRUE-LIST-LISTP-FORWARD-TO-TRUE-LISTP-ASSOC-EQ", "ACL2-USER", "ACL2"), 691("TRUE-LISTP-CADR-ASSOC-EQ-FOR-OPEN-CHANNELS-P", "ACL2-USER", "ACL2"), 692("TRUE-LISTP-UPDATE-NTH", "ACL2-USER", "ACL2"), 693("TYPED-IO-LISTP", "ACL2-USER", "ACL2"), 694("TYPED-IO-LISTP-FORWARD-TO-TRUE-LISTP", "ACL2-USER", "ACL2"), 695("U", "ACL2-USER", "ACL2"), 696("UBT", "ACL2-USER", "ACL2"), 697("UBT!", "ACL2-USER", "ACL2"), 698("UNARY--", "ACL2-USER", "ACL2"), 699("UNARY-/", "ACL2-USER", "ACL2"), 700("UNARY-FUNCTION-SYMBOL-LISTP", "ACL2-USER", "ACL2"), 701("UNICITY-OF-0", "ACL2-USER", "ACL2"), 702("UNICITY-OF-1", "ACL2-USER", "ACL2"), 703("UNION-EQ", "ACL2-USER", "ACL2"), 704("UNION-EQUAL", "ACL2-USER", "ACL2"), 705("UNION-THEORIES", "ACL2-USER", "ACL2"), 706("UNIVERSAL-THEORY", "ACL2-USER", "ACL2"), 707("UNMONITOR", "ACL2-USER", "ACL2"), 708("UNSAVE", "ACL2-USER", "ACL2"), 709("UNTRACE$", "ACL2-USER", "ACL2"), 710("UPDATE-32-BIT-INTEGER-STACK", "ACL2-USER", "ACL2"), 711("UPDATE-BIG-CLOCK-ENTRY", "ACL2-USER", "ACL2"), 712("UPDATE-FILE-CLOCK", "ACL2-USER", "ACL2"), 713("UPDATE-GLOBAL-TABLE", "ACL2-USER", "ACL2"), 714("UPDATE-IDATES", "ACL2-USER", "ACL2"), 715("UPDATE-LIST-ALL-PACKAGE-NAMES-LST", "ACL2-USER", "ACL2"), 716("UPDATE-NTH", "ACL2-USER", "ACL2"), 717("UPDATE-OPEN-INPUT-CHANNELS", "ACL2-USER", "ACL2"), 718("UPDATE-OPEN-OUTPUT-CHANNELS", "ACL2-USER", "ACL2"), 719("UPDATE-READ-FILES", "ACL2-USER", "ACL2"), 720("UPDATE-RUN-TIMES", "ACL2-USER", "ACL2"), 721("UPDATE-RUN-TIMES-PRESERVES-STATE-P1", "ACL2-USER", "ACL2"), 722("UPDATE-T-STACK", "ACL2-USER", "ACL2"), 723("UPDATE-USER-STOBJ-ALIST", "ACL2-USER", "ACL2"), 724("UPDATE-USER-STOBJ-ALIST1", "ACL2-USER", "ACL2"), 725("UPDATE-WRITTEN-FILES", "ACL2-USER", "ACL2"), 726("UPPER-CASE-P-CHAR-UPCASE", "ACL2-USER", "ACL2"), 727("UPPER-CASE-P-FORWARD-TO-ALPHA-CHAR-P", "ACL2-USER", "ACL2"), 728("USER-STOBJ-ALIST", "ACL2-USER", "ACL2"), 729("USER-STOBJ-ALIST1", "ACL2-USER", "ACL2"), 730("VERBOSE-PSTACK", "ACL2-USER", "ACL2"), 731("VERIFY", "ACL2-USER", "ACL2"), 732("VERIFY-GUARDS", "ACL2-USER", "ACL2"), 733("VERIFY-TERMINATION", "ACL2-USER", "ACL2"), 734("W", "ACL2-USER", "ACL2"), 735("WARNING!", "ACL2-USER", "ACL2"), 736("WET", "ACL2-USER", "ACL2"), 737("WITH-OUTPUT", "ACL2-USER", "ACL2"), 738("WORLD", "ACL2-USER", "ACL2"), 739("WORLDP", "ACL2-USER", "ACL2"), 740("WORLDP-FORWARD-TO-ASSOC-EQ-EQUAL-ALISTP", "ACL2-USER", "ACL2"), 741("WORMHOLE", "ACL2-USER", "ACL2"), 742("WORMHOLE1", "ACL2-USER", "ACL2"), 743("WRITABLE-FILE-LISTP", "ACL2-USER", "ACL2"), 744("WRITABLE-FILE-LISTP-FORWARD-TO-TRUE-LIST-LISTP", "ACL2-USER", "ACL2"), 745("WRITABLE-FILE-LISTP1", "ACL2-USER", "ACL2"), 746("WRITABLE-FILE-LISTP1-FORWARD-TO-TRUE-LISTP-AND-CONSP", "ACL2-USER", 747"ACL2"), 748("WRITE-BYTE$", "ACL2-USER", "ACL2"), 749("WRITEABLE-FILES", "ACL2-USER", "ACL2"), 750("WRITEABLE-FILES-P", "ACL2-USER", "ACL2"), 751("WRITEABLE-FILES-P-FORWARD-TO-WRITABLE-FILE-LISTP", "ACL2-USER", "ACL2"), 752("WRITTEN-FILE", "ACL2-USER", "ACL2"), 753("WRITTEN-FILE-FORWARD-TO-TRUE-LISTP-AND-CONSP", "ACL2-USER", "ACL2"), 754("WRITTEN-FILE-LISTP", "ACL2-USER", "ACL2"), 755("WRITTEN-FILE-LISTP-FORWARD-TO-TRUE-LIST-LISTP-AND-ALISTP", "ACL2-USER", 756"ACL2"), 757("WRITTEN-FILES", "ACL2-USER", "ACL2"), 758("WRITTEN-FILES-P", "ACL2-USER", "ACL2"), 759("WRITTEN-FILES-P-FORWARD-TO-WRITTEN-FILE-LISTP", "ACL2-USER", "ACL2"), 760("XARGS", "ACL2-USER", "ACL2"), 761("XXXJOIN", "ACL2-USER", "ACL2"), 762("ZERO", "ACL2-USER", "ACL2"), 763("ZIP", "ACL2-USER", "ACL2"), 764("ZP", "ACL2-USER", "ACL2"), 765("&ALLOW-OTHER-KEYS", "ACL2-USER", "COMMON-LISP"), 766("*PRINT-MISER-WIDTH*", "ACL2-USER", "COMMON-LISP"), 767("&AUX", "ACL2-USER", "COMMON-LISP"), 768("*PRINT-PPRINT-DISPATCH*", "ACL2-USER", "COMMON-LISP"), 769("&BODY", "ACL2-USER", "COMMON-LISP"), 770("*PRINT-PRETTY*", "ACL2-USER", "COMMON-LISP"), 771("&ENVIRONMENT", "ACL2-USER", "COMMON-LISP"), 772("*PRINT-RADIX*", "ACL2-USER", "COMMON-LISP"), 773("&KEY", "ACL2-USER", "COMMON-LISP"), 774("*PRINT-READABLY*", "ACL2-USER", "COMMON-LISP"), 775("&OPTIONAL", "ACL2-USER", "COMMON-LISP"), 776("*PRINT-RIGHT-MARGIN*", "ACL2-USER", "COMMON-LISP"), 777("&REST", "ACL2-USER", "COMMON-LISP"), 778("*QUERY-IO*", "ACL2-USER", "COMMON-LISP"), 779("&WHOLE", "ACL2-USER", "COMMON-LISP"), 780("*RANDOM-STATE*", "ACL2-USER", "COMMON-LISP"), 781("*", "ACL2-USER", "COMMON-LISP"), 782("*READ-BASE*", "ACL2-USER", "COMMON-LISP"), 783("**", "ACL2-USER", "COMMON-LISP"), 784("*READ-DEFAULT-FLOAT-FORMAT*", "ACL2-USER", "COMMON-LISP"), 785("***", "ACL2-USER", "COMMON-LISP"), 786("*READ-EVAL*", "ACL2-USER", "COMMON-LISP"), 787("*BREAK-ON-SIGNALS*", "ACL2-USER", "COMMON-LISP"), 788("*READ-SUPPRESS*", "ACL2-USER", "COMMON-LISP"), 789("*COMPILE-FILE-PATHNAME*", "ACL2-USER", "COMMON-LISP"), 790("*READTABLE*", "ACL2-USER", "COMMON-LISP"), 791("*COMPILE-FILE-TRUENAME*", "ACL2-USER", "COMMON-LISP"), 792("*STANDARD-INPUT*", "ACL2-USER", "COMMON-LISP"), 793("*COMPILE-PRINT*", "ACL2-USER", "COMMON-LISP"), 794("*STANDARD-OUTPUT*", "ACL2-USER", "COMMON-LISP"), 795("*COMPILE-VERBOSE*", "ACL2-USER", "COMMON-LISP"), 796("*TERMINAL-IO*", "ACL2-USER", "COMMON-LISP"), 797("*DEBUG-IO*", "ACL2-USER", "COMMON-LISP"), 798("*TRACE-OUTPUT*", "ACL2-USER", "COMMON-LISP"), 799("*DEBUGGER-HOOK*", "ACL2-USER", "COMMON-LISP"), 800("+", "ACL2-USER", "COMMON-LISP"), 801("*DEFAULT-PATHNAME-DEFAULTS*", "ACL2-USER", "COMMON-LISP"), 802("++", "ACL2-USER", "COMMON-LISP"), 803("*ERROR-OUTPUT*", "ACL2-USER", "COMMON-LISP"), 804("+++", "ACL2-USER", "COMMON-LISP"), 805("*FEATURES*", "ACL2-USER", "COMMON-LISP"), 806("-", "ACL2-USER", "COMMON-LISP"), 807("*GENSYM-COUNTER*", "ACL2-USER", "COMMON-LISP"), 808("/", "ACL2-USER", "COMMON-LISP"), 809("*LOAD-PATHNAME*", "ACL2-USER", "COMMON-LISP"), 810("//", "ACL2-USER", "COMMON-LISP"), 811("*LOAD-PRINT*", "ACL2-USER", "COMMON-LISP"), 812("///", "ACL2-USER", "COMMON-LISP"), 813("*LOAD-TRUENAME*", "ACL2-USER", "COMMON-LISP"), 814("/=", "ACL2-USER", "COMMON-LISP"), 815("*LOAD-VERBOSE*", "ACL2-USER", "COMMON-LISP"), 816("1+", "ACL2-USER", "COMMON-LISP"), 817("*MACROEXPAND-HOOK*", "ACL2-USER", "COMMON-LISP"), 818("1-", "ACL2-USER", "COMMON-LISP"), 819("*MODULES*", "ACL2-USER", "COMMON-LISP"), 820("<", "ACL2-USER", "COMMON-LISP"), 821("*PACKAGE*", "ACL2-USER", "COMMON-LISP"), 822("<=", "ACL2-USER", "COMMON-LISP"), 823("*PRINT-ARRAY*", "ACL2-USER", "COMMON-LISP"), 824("=", "ACL2-USER", "COMMON-LISP"), 825("*PRINT-BASE*", "ACL2-USER", "COMMON-LISP"), 826(">", "ACL2-USER", "COMMON-LISP"), 827("*PRINT-CASE*", "ACL2-USER", "COMMON-LISP"), 828(">=", "ACL2-USER", "COMMON-LISP"), 829("*PRINT-CIRCLE*", "ACL2-USER", "COMMON-LISP"), 830("ABORT", "ACL2-USER", "COMMON-LISP"), 831("*PRINT-ESCAPE*", "ACL2-USER", "COMMON-LISP"), 832("ABS", "ACL2-USER", "COMMON-LISP"), 833("*PRINT-GENSYM*", "ACL2-USER", "COMMON-LISP"), 834("ACONS", "ACL2-USER", "COMMON-LISP"), 835("*PRINT-LENGTH*", "ACL2-USER", "COMMON-LISP"), 836("ACOS", "ACL2-USER", "COMMON-LISP"), 837("*PRINT-LEVEL*", "ACL2-USER", "COMMON-LISP"), 838("ACOSH", "ACL2-USER", "COMMON-LISP"), 839("*PRINT-LINES*", "ACL2-USER", "COMMON-LISP"), 840("ADD-METHOD", "ACL2-USER", "COMMON-LISP"), 841("ADJOIN", "ACL2-USER", "COMMON-LISP"), 842("ATOM", "ACL2-USER", "COMMON-LISP"), 843("BOUNDP", "ACL2-USER", "COMMON-LISP"), 844("ADJUST-ARRAY", "ACL2-USER", "COMMON-LISP"), 845("BASE-CHAR", "ACL2-USER", "COMMON-LISP"), 846("BREAK", "ACL2-USER", "COMMON-LISP"), 847("ADJUSTABLE-ARRAY-P", "ACL2-USER", "COMMON-LISP"), 848("BASE-STRING", "ACL2-USER", "COMMON-LISP"), 849("BROADCAST-STREAM", "ACL2-USER", "COMMON-LISP"), 850("ALLOCATE-INSTANCE", "ACL2-USER", "COMMON-LISP"), 851("BIGNUM", "ACL2-USER", "COMMON-LISP"), 852("BROADCAST-STREAM-STREAMS", "ACL2-USER", "COMMON-LISP"), 853("ALPHA-CHAR-P", "ACL2-USER", "COMMON-LISP"), 854("BIT", "ACL2-USER", "COMMON-LISP"), 855("BUILT-IN-CLASS", "ACL2-USER", "COMMON-LISP"), 856("ALPHANUMERICP", "ACL2-USER", "COMMON-LISP"), 857("BIT-AND", "ACL2-USER", "COMMON-LISP"), 858("BUTLAST", "ACL2-USER", "COMMON-LISP"), 859("AND", "ACL2-USER", "COMMON-LISP"), 860("BIT-ANDC1", "ACL2-USER", "COMMON-LISP"), 861("BYTE", "ACL2-USER", "COMMON-LISP"), 862("APPEND", "ACL2-USER", "COMMON-LISP"), 863("BIT-ANDC2", "ACL2-USER", "COMMON-LISP"), 864("BYTE-POSITION", "ACL2-USER", "COMMON-LISP"), 865("APPLY", "ACL2-USER", "COMMON-LISP"), 866("BIT-EQV", "ACL2-USER", "COMMON-LISP"), 867("BYTE-SIZE", "ACL2-USER", "COMMON-LISP"), 868("APROPOS", "ACL2-USER", "COMMON-LISP"), 869("BIT-IOR", "ACL2-USER", "COMMON-LISP"), 870("CAAAAR", "ACL2-USER", "COMMON-LISP"), 871("APROPOS-LIST", "ACL2-USER", "COMMON-LISP"), 872("BIT-NAND", "ACL2-USER", "COMMON-LISP"), 873("CAAADR", "ACL2-USER", "COMMON-LISP"), 874("AREF", "ACL2-USER", "COMMON-LISP"), 875("BIT-NOR", "ACL2-USER", "COMMON-LISP"), 876("CAAAR", "ACL2-USER", "COMMON-LISP"), 877("ARITHMETIC-ERROR", "ACL2-USER", "COMMON-LISP"), 878("BIT-NOT", "ACL2-USER", "COMMON-LISP"), 879("CAADAR", "ACL2-USER", "COMMON-LISP"), 880("ARITHMETIC-ERROR-OPERANDS", "ACL2-USER", "COMMON-LISP"), 881("BIT-ORC1", "ACL2-USER", "COMMON-LISP"), 882("CAADDR", "ACL2-USER", "COMMON-LISP"), 883("ARITHMETIC-ERROR-OPERATION", "ACL2-USER", "COMMON-LISP"), 884("BIT-ORC2", "ACL2-USER", "COMMON-LISP"), 885("CAADR", "ACL2-USER", "COMMON-LISP"), 886("ARRAY", "ACL2-USER", "COMMON-LISP"), 887("BIT-VECTOR", "ACL2-USER", "COMMON-LISP"), 888("CAAR", "ACL2-USER", "COMMON-LISP"), 889("ARRAY-DIMENSION", "ACL2-USER", "COMMON-LISP"), 890("BIT-VECTOR-P", "ACL2-USER", "COMMON-LISP"), 891("CADAAR", "ACL2-USER", "COMMON-LISP"), 892("ARRAY-DIMENSION-LIMIT", "ACL2-USER", "COMMON-LISP"), 893("BIT-XOR", "ACL2-USER", "COMMON-LISP"), 894("CADADR", "ACL2-USER", "COMMON-LISP"), 895("ARRAY-DIMENSIONS", "ACL2-USER", "COMMON-LISP"), 896("BLOCK", "ACL2-USER", "COMMON-LISP"), 897("CADAR", "ACL2-USER", "COMMON-LISP"), 898("ARRAY-DISPLACEMENT", "ACL2-USER", "COMMON-LISP"), 899("BOOLE", "ACL2-USER", "COMMON-LISP"), 900("CADDAR", "ACL2-USER", "COMMON-LISP"), 901("ARRAY-ELEMENT-TYPE", "ACL2-USER", "COMMON-LISP"), 902("BOOLE-1", "ACL2-USER", "COMMON-LISP"), 903("CADDDR", "ACL2-USER", "COMMON-LISP"), 904("ARRAY-HAS-FILL-POINTER-P", "ACL2-USER", "COMMON-LISP"), 905("BOOLE-2", "ACL2-USER", "COMMON-LISP"), 906("CADDR", "ACL2-USER", "COMMON-LISP"), 907("ARRAY-IN-BOUNDS-P", "ACL2-USER", "COMMON-LISP"), 908("BOOLE-AND", "ACL2-USER", "COMMON-LISP"), 909("CADR", "ACL2-USER", "COMMON-LISP"), 910("ARRAY-RANK", "ACL2-USER", "COMMON-LISP"), 911("BOOLE-ANDC1", "ACL2-USER", "COMMON-LISP"), 912("CALL-ARGUMENTS-LIMIT", "ACL2-USER", "COMMON-LISP"), 913("ARRAY-RANK-LIMIT", "ACL2-USER", "COMMON-LISP"), 914("BOOLE-ANDC2", "ACL2-USER", "COMMON-LISP"), 915("CALL-METHOD", "ACL2-USER", "COMMON-LISP"), 916("ARRAY-ROW-MAJOR-INDEX", "ACL2-USER", "COMMON-LISP"), 917("BOOLE-C1", "ACL2-USER", "COMMON-LISP"), 918("CALL-NEXT-METHOD", "ACL2-USER", "COMMON-LISP"), 919("ARRAY-TOTAL-SIZE", "ACL2-USER", "COMMON-LISP"), 920("BOOLE-C2", "ACL2-USER", "COMMON-LISP"), 921("CAR", "ACL2-USER", "COMMON-LISP"), 922("ARRAY-TOTAL-SIZE-LIMIT", "ACL2-USER", "COMMON-LISP"), 923("BOOLE-CLR", "ACL2-USER", "COMMON-LISP"), 924("CASE", "ACL2-USER", "COMMON-LISP"), 925("ARRAYP", "ACL2-USER", "COMMON-LISP"), 926("BOOLE-EQV", "ACL2-USER", "COMMON-LISP"), 927("CATCH", "ACL2-USER", "COMMON-LISP"), 928("ASH", "ACL2-USER", "COMMON-LISP"), 929("BOOLE-IOR", "ACL2-USER", "COMMON-LISP"), 930("CCASE", "ACL2-USER", "COMMON-LISP"), 931("ASIN", "ACL2-USER", "COMMON-LISP"), 932("BOOLE-NAND", "ACL2-USER", "COMMON-LISP"), 933("CDAAAR", "ACL2-USER", "COMMON-LISP"), 934("ASINH", "ACL2-USER", "COMMON-LISP"), 935("BOOLE-NOR", "ACL2-USER", "COMMON-LISP"), 936("CDAADR", "ACL2-USER", "COMMON-LISP"), 937("ASSERT", "ACL2-USER", "COMMON-LISP"), 938("BOOLE-ORC1", "ACL2-USER", "COMMON-LISP"), 939("CDAAR", "ACL2-USER", "COMMON-LISP"), 940("ASSOC", "ACL2-USER", "COMMON-LISP"), 941("BOOLE-ORC2", "ACL2-USER", "COMMON-LISP"), 942("CDADAR", "ACL2-USER", "COMMON-LISP"), 943("ASSOC-IF", "ACL2-USER", "COMMON-LISP"), 944("BOOLE-SET", "ACL2-USER", "COMMON-LISP"), 945("CDADDR", "ACL2-USER", "COMMON-LISP"), 946("ASSOC-IF-NOT", "ACL2-USER", "COMMON-LISP"), 947("BOOLE-XOR", "ACL2-USER", "COMMON-LISP"), 948("CDADR", "ACL2-USER", "COMMON-LISP"), 949("ATAN", "ACL2-USER", "COMMON-LISP"), 950("BOOLEAN", "ACL2-USER", "COMMON-LISP"), 951("CDAR", "ACL2-USER", "COMMON-LISP"), 952("ATANH", "ACL2-USER", "COMMON-LISP"), 953("BOTH-CASE-P", "ACL2-USER", "COMMON-LISP"), 954("CDDAAR", "ACL2-USER", "COMMON-LISP"), 955("CDDADR", "ACL2-USER", "COMMON-LISP"), 956("CLEAR-INPUT", "ACL2-USER", "COMMON-LISP"), 957("COPY-TREE", "ACL2-USER", "COMMON-LISP"), 958("CDDAR", "ACL2-USER", "COMMON-LISP"), 959("CLEAR-OUTPUT", "ACL2-USER", "COMMON-LISP"), 960("COS", "ACL2-USER", "COMMON-LISP"), 961("CDDDAR", "ACL2-USER", "COMMON-LISP"), 962("CLOSE", "ACL2-USER", "COMMON-LISP"), 963("COSH", "ACL2-USER", "COMMON-LISP"), 964("CDDDDR", "ACL2-USER", "COMMON-LISP"), 965("CLRHASH", "ACL2-USER", "COMMON-LISP"), 966("COUNT", "ACL2-USER", "COMMON-LISP"), 967("CDDDR", "ACL2-USER", "COMMON-LISP"), 968("CODE-CHAR", "ACL2-USER", "COMMON-LISP"), 969("COUNT-IF", "ACL2-USER", "COMMON-LISP"), 970("CDDR", "ACL2-USER", "COMMON-LISP"), 971("COERCE", "ACL2-USER", "COMMON-LISP"), 972("COUNT-IF-NOT", "ACL2-USER", "COMMON-LISP"), 973("CDR", "ACL2-USER", "COMMON-LISP"), 974("COMPILATION-SPEED", "ACL2-USER", "COMMON-LISP"), 975("CTYPECASE", "ACL2-USER", "COMMON-LISP"), 976("CEILING", "ACL2-USER", "COMMON-LISP"), 977("COMPILE", "ACL2-USER", "COMMON-LISP"), 978("DEBUG", "ACL2-USER", "COMMON-LISP"), 979("CELL-ERROR", "ACL2-USER", "COMMON-LISP"), 980("COMPILE-FILE", "ACL2-USER", "COMMON-LISP"), 981("DECF", "ACL2-USER", "COMMON-LISP"), 982("CELL-ERROR-NAME", "ACL2-USER", "COMMON-LISP"), 983("COMPILE-FILE-PATHNAME", "ACL2-USER", "COMMON-LISP"), 984("DECLAIM", "ACL2-USER", "COMMON-LISP"), 985("CERROR", "ACL2-USER", "COMMON-LISP"), 986("COMPILED-FUNCTION", "ACL2-USER", "COMMON-LISP"), 987("DECLARATION", "ACL2-USER", "COMMON-LISP"), 988("CHANGE-CLASS", "ACL2-USER", "COMMON-LISP"), 989("COMPILED-FUNCTION-P", "ACL2-USER", "COMMON-LISP"), 990("DECLARE", "ACL2-USER", "COMMON-LISP"), 991("CHAR", "ACL2-USER", "COMMON-LISP"), 992("COMPILER-MACRO", "ACL2-USER", "COMMON-LISP"), 993("DECODE-FLOAT", "ACL2-USER", "COMMON-LISP"), 994("CHAR-CODE", "ACL2-USER", "COMMON-LISP"), 995("COMPILER-MACRO-FUNCTION", "ACL2-USER", "COMMON-LISP"), 996("DECODE-UNIVERSAL-TIME", "ACL2-USER", "COMMON-LISP"), 997("CHAR-CODE-LIMIT", "ACL2-USER", "COMMON-LISP"), 998("COMPLEMENT", "ACL2-USER", "COMMON-LISP"), 999("DEFCLASS", "ACL2-USER", "COMMON-LISP"), 1000("CHAR-DOWNCASE", "ACL2-USER", "COMMON-LISP"), 1001("COMPLEX", "ACL2-USER", "COMMON-LISP"), 1002("DEFCONSTANT", "ACL2-USER", "COMMON-LISP"), 1003("CHAR-EQUAL", "ACL2-USER", "COMMON-LISP"), 1004("COMPLEXP", "ACL2-USER", "COMMON-LISP"), 1005("DEFGENERIC", "ACL2-USER", "COMMON-LISP"), 1006("CHAR-GREATERP", "ACL2-USER", "COMMON-LISP"), 1007("COMPUTE-APPLICABLE-METHODS", "ACL2-USER", "COMMON-LISP"), 1008("DEFINE-COMPILER-MACRO", "ACL2-USER", "COMMON-LISP"), 1009("CHAR-INT", "ACL2-USER", "COMMON-LISP"), 1010("COMPUTE-RESTARTS", "ACL2-USER", "COMMON-LISP"), 1011("DEFINE-CONDITION", "ACL2-USER", "COMMON-LISP"), 1012("CHAR-LESSP", "ACL2-USER", "COMMON-LISP"), 1013("CONCATENATE", "ACL2-USER", "COMMON-LISP"), 1014("DEFINE-METHOD-COMBINATION", "ACL2-USER", "COMMON-LISP"), 1015("CHAR-NAME", "ACL2-USER", "COMMON-LISP"), 1016("CONCATENATED-STREAM", "ACL2-USER", "COMMON-LISP"), 1017("DEFINE-MODIFY-MACRO", "ACL2-USER", "COMMON-LISP"), 1018("CHAR-NOT-EQUAL", "ACL2-USER", "COMMON-LISP"), 1019("CONCATENATED-STREAM-STREAMS", "ACL2-USER", "COMMON-LISP"), 1020("DEFINE-SETF-EXPANDER", "ACL2-USER", "COMMON-LISP"), 1021("CHAR-NOT-GREATERP", "ACL2-USER", "COMMON-LISP"), 1022("COND", "ACL2-USER", "COMMON-LISP"), 1023("DEFINE-SYMBOL-MACRO", "ACL2-USER", "COMMON-LISP"), 1024("CHAR-NOT-LESSP", "ACL2-USER", "COMMON-LISP"), 1025("CONDITION", "ACL2-USER", "COMMON-LISP"), 1026("DEFMACRO", "ACL2-USER", "COMMON-LISP"), 1027("CHAR-UPCASE", "ACL2-USER", "COMMON-LISP"), 1028("CONJUGATE", "ACL2-USER", "COMMON-LISP"), 1029("DEFMETHOD", "ACL2-USER", "COMMON-LISP"), 1030("CHAR/=", "ACL2-USER", "COMMON-LISP"), 1031("CONS", "ACL2-USER", "COMMON-LISP"), 1032("DEFPACKAGE", "ACL2-USER", "COMMON-LISP"), 1033("CHAR<", "ACL2-USER", "COMMON-LISP"), 1034("CONSP", "ACL2-USER", "COMMON-LISP"), 1035("DEFPARAMETER", "ACL2-USER", "COMMON-LISP"), 1036("CHAR<=", "ACL2-USER", "COMMON-LISP"), 1037("CONSTANTLY", "ACL2-USER", "COMMON-LISP"), 1038("DEFSETF", "ACL2-USER", "COMMON-LISP"), 1039("CHAR=", "ACL2-USER", "COMMON-LISP"), 1040("CONSTANTP", "ACL2-USER", "COMMON-LISP"), 1041("DEFSTRUCT", "ACL2-USER", "COMMON-LISP"), 1042("CHAR>", "ACL2-USER", "COMMON-LISP"), 1043("CONTINUE", "ACL2-USER", "COMMON-LISP"), 1044("DEFTYPE", "ACL2-USER", "COMMON-LISP"), 1045("CHAR>=", "ACL2-USER", "COMMON-LISP"), 1046("CONTROL-ERROR", "ACL2-USER", "COMMON-LISP"), 1047("DEFUN", "ACL2-USER", "COMMON-LISP"), 1048("CHARACTER", "ACL2-USER", "COMMON-LISP"), 1049("COPY-ALIST", "ACL2-USER", "COMMON-LISP"), 1050("DEFVAR", "ACL2-USER", "COMMON-LISP"), 1051("CHARACTERP", "ACL2-USER", "COMMON-LISP"), 1052("COPY-LIST", "ACL2-USER", "COMMON-LISP"), 1053("DELETE", "ACL2-USER", "COMMON-LISP"), 1054("CHECK-TYPE", "ACL2-USER", "COMMON-LISP"), 1055("COPY-PPRINT-DISPATCH", "ACL2-USER", "COMMON-LISP"), 1056("DELETE-DUPLICATES", "ACL2-USER", "COMMON-LISP"), 1057("CIS", "ACL2-USER", "COMMON-LISP"), 1058("COPY-READTABLE", "ACL2-USER", "COMMON-LISP"), 1059("DELETE-FILE", "ACL2-USER", "COMMON-LISP"), 1060("CLASS", "ACL2-USER", "COMMON-LISP"), 1061("COPY-SEQ", "ACL2-USER", "COMMON-LISP"), 1062("DELETE-IF", "ACL2-USER", "COMMON-LISP"), 1063("CLASS-NAME", "ACL2-USER", "COMMON-LISP"), 1064("COPY-STRUCTURE", "ACL2-USER", "COMMON-LISP"), 1065("DELETE-IF-NOT", "ACL2-USER", "COMMON-LISP"), 1066("CLASS-OF", "ACL2-USER", "COMMON-LISP"), 1067("COPY-SYMBOL", "ACL2-USER", "COMMON-LISP"), 1068("DELETE-PACKAGE", "ACL2-USER", "COMMON-LISP"), 1069("DENOMINATOR", "ACL2-USER", "COMMON-LISP"), 1070("EQ", "ACL2-USER", "COMMON-LISP"), 1071("DEPOSIT-FIELD", "ACL2-USER", "COMMON-LISP"), 1072("EQL", "ACL2-USER", "COMMON-LISP"), 1073("DESCRIBE", "ACL2-USER", "COMMON-LISP"), 1074("EQUAL", "ACL2-USER", "COMMON-LISP"), 1075("DESCRIBE-OBJECT", "ACL2-USER", "COMMON-LISP"), 1076("EQUALP", "ACL2-USER", "COMMON-LISP"), 1077("DESTRUCTURING-BIND", "ACL2-USER", "COMMON-LISP"), 1078("ERROR", "ACL2-USER", "COMMON-LISP"), 1079("DIGIT-CHAR", "ACL2-USER", "COMMON-LISP"), 1080("ETYPECASE", "ACL2-USER", "COMMON-LISP"), 1081("DIGIT-CHAR-P", "ACL2-USER", "COMMON-LISP"), 1082("EVAL", "ACL2-USER", "COMMON-LISP"), 1083("DIRECTORY", "ACL2-USER", "COMMON-LISP"), 1084("EVAL-WHEN", "ACL2-USER", "COMMON-LISP"), 1085("DIRECTORY-NAMESTRING", "ACL2-USER", "COMMON-LISP"), 1086("EVENP", "ACL2-USER", "COMMON-LISP"), 1087("DISASSEMBLE", "ACL2-USER", "COMMON-LISP"), 1088("EVERY", "ACL2-USER", "COMMON-LISP"), 1089("DIVISION-BY-ZERO", "ACL2-USER", "COMMON-LISP"), 1090("EXP", "ACL2-USER", "COMMON-LISP"), 1091("DO", "ACL2-USER", "COMMON-LISP"), 1092("EXPORT", "ACL2-USER", "COMMON-LISP"), 1093("DO*", "ACL2-USER", "COMMON-LISP"), 1094("EXPT", "ACL2-USER", "COMMON-LISP"), 1095("DO-ALL-SYMBOLS", "ACL2-USER", "COMMON-LISP"), 1096("EXTENDED-CHAR", "ACL2-USER", "COMMON-LISP"), 1097("DO-EXTERNAL-SYMBOLS", "ACL2-USER", "COMMON-LISP"), 1098("FBOUNDP", "ACL2-USER", "COMMON-LISP"), 1099("DO-SYMBOLS", "ACL2-USER", "COMMON-LISP"), 1100("FCEILING", "ACL2-USER", "COMMON-LISP"), 1101("DOCUMENTATION", "ACL2-USER", "COMMON-LISP"), 1102("FDEFINITION", "ACL2-USER", "COMMON-LISP"), 1103("DOLIST", "ACL2-USER", "COMMON-LISP"), 1104("FFLOOR", "ACL2-USER", "COMMON-LISP"), 1105("DOTIMES", "ACL2-USER", "COMMON-LISP"), 1106("FIFTH", "ACL2-USER", "COMMON-LISP"), 1107("DOUBLE-FLOAT", "ACL2-USER", "COMMON-LISP"), 1108("FILE-AUTHOR", "ACL2-USER", "COMMON-LISP"), 1109("DOUBLE-FLOAT-EPSILON", "ACL2-USER", "COMMON-LISP"), 1110("FILE-ERROR", "ACL2-USER", "COMMON-LISP"), 1111("DOUBLE-FLOAT-NEGATIVE-EPSILON", "ACL2-USER", "COMMON-LISP"), 1112("FILE-ERROR-PATHNAME", "ACL2-USER", "COMMON-LISP"), 1113("DPB", "ACL2-USER", "COMMON-LISP"), 1114("FILE-LENGTH", "ACL2-USER", "COMMON-LISP"), 1115("DRIBBLE", "ACL2-USER", "COMMON-LISP"), 1116("FILE-NAMESTRING", "ACL2-USER", "COMMON-LISP"), 1117("DYNAMIC-EXTENT", "ACL2-USER", "COMMON-LISP"), 1118("FILE-POSITION", "ACL2-USER", "COMMON-LISP"), 1119("ECASE", "ACL2-USER", "COMMON-LISP"), 1120("FILE-STREAM", "ACL2-USER", "COMMON-LISP"), 1121("ECHO-STREAM", "ACL2-USER", "COMMON-LISP"), 1122("FILE-STRING-LENGTH", "ACL2-USER", "COMMON-LISP"), 1123("ECHO-STREAM-INPUT-STREAM", "ACL2-USER", "COMMON-LISP"), 1124("FILE-WRITE-DATE", "ACL2-USER", "COMMON-LISP"), 1125("ECHO-STREAM-OUTPUT-STREAM", "ACL2-USER", "COMMON-LISP"), 1126("FILL", "ACL2-USER", "COMMON-LISP"), 1127("ED", "ACL2-USER", "COMMON-LISP"), 1128("FILL-POINTER", "ACL2-USER", "COMMON-LISP"), 1129("EIGHTH", "ACL2-USER", "COMMON-LISP"), 1130("FIND", "ACL2-USER", "COMMON-LISP"), 1131("ELT", "ACL2-USER", "COMMON-LISP"), 1132("FIND-ALL-SYMBOLS", "ACL2-USER", "COMMON-LISP"), 1133("ENCODE-UNIVERSAL-TIME", "ACL2-USER", "COMMON-LISP"), 1134("FIND-CLASS", "ACL2-USER", "COMMON-LISP"), 1135("END-OF-FILE", "ACL2-USER", "COMMON-LISP"), 1136("FIND-IF", "ACL2-USER", "COMMON-LISP"), 1137("ENDP", "ACL2-USER", "COMMON-LISP"), 1138("FIND-IF-NOT", "ACL2-USER", "COMMON-LISP"), 1139("ENOUGH-NAMESTRING", "ACL2-USER", "COMMON-LISP"), 1140("FIND-METHOD", "ACL2-USER", "COMMON-LISP"), 1141("ENSURE-DIRECTORIES-EXIST", "ACL2-USER", "COMMON-LISP"), 1142("FIND-PACKAGE", "ACL2-USER", "COMMON-LISP"), 1143("ENSURE-GENERIC-FUNCTION", "ACL2-USER", "COMMON-LISP"), 1144("FIND-RESTART", "ACL2-USER", "COMMON-LISP"), 1145("FIND-SYMBOL", "ACL2-USER", "COMMON-LISP"), 1146("GET-INTERNAL-RUN-TIME", "ACL2-USER", "COMMON-LISP"), 1147("FINISH-OUTPUT", "ACL2-USER", "COMMON-LISP"), 1148("GET-MACRO-CHARACTER", "ACL2-USER", "COMMON-LISP"), 1149("FIRST", "ACL2-USER", "COMMON-LISP"), 1150("GET-OUTPUT-STREAM-STRING", "ACL2-USER", "COMMON-LISP"), 1151("FIXNUM", "ACL2-USER", "COMMON-LISP"), 1152("GET-PROPERTIES", "ACL2-USER", "COMMON-LISP"), 1153("FLET", "ACL2-USER", "COMMON-LISP"), 1154("GET-SETF-EXPANSION", "ACL2-USER", "COMMON-LISP"), 1155("FLOAT", "ACL2-USER", "COMMON-LISP"), 1156("GET-UNIVERSAL-TIME", "ACL2-USER", "COMMON-LISP"), 1157("FLOAT-DIGITS", "ACL2-USER", "COMMON-LISP"), 1158("GETF", "ACL2-USER", "COMMON-LISP"), 1159("FLOAT-PRECISION", "ACL2-USER", "COMMON-LISP"), 1160("GETHASH", "ACL2-USER", "COMMON-LISP"), 1161("FLOAT-RADIX", "ACL2-USER", "COMMON-LISP"), 1162("GO", "ACL2-USER", "COMMON-LISP"), 1163("FLOAT-SIGN", "ACL2-USER", "COMMON-LISP"), 1164("GRAPHIC-CHAR-P", "ACL2-USER", "COMMON-LISP"), 1165("FLOATING-POINT-INEXACT", "ACL2-USER", "COMMON-LISP"), 1166("HANDLER-BIND", "ACL2-USER", "COMMON-LISP"), 1167("FLOATING-POINT-INVALID-OPERATION", "ACL2-USER", "COMMON-LISP"), 1168("HANDLER-CASE", "ACL2-USER", "COMMON-LISP"), 1169("FLOATING-POINT-OVERFLOW", "ACL2-USER", "COMMON-LISP"), 1170("HASH-TABLE", "ACL2-USER", "COMMON-LISP"), 1171("FLOATING-POINT-UNDERFLOW", "ACL2-USER", "COMMON-LISP"), 1172("HASH-TABLE-COUNT", "ACL2-USER", "COMMON-LISP"), 1173("FLOATP", "ACL2-USER", "COMMON-LISP"), 1174("HASH-TABLE-P", "ACL2-USER", "COMMON-LISP"), 1175("FLOOR", "ACL2-USER", "COMMON-LISP"), 1176("HASH-TABLE-REHASH-SIZE", "ACL2-USER", "COMMON-LISP"), 1177("FMAKUNBOUND", "ACL2-USER", "COMMON-LISP"), 1178("HASH-TABLE-REHASH-THRESHOLD", "ACL2-USER", "COMMON-LISP"), 1179("FORCE-OUTPUT", "ACL2-USER", "COMMON-LISP"), 1180("HASH-TABLE-SIZE", "ACL2-USER", "COMMON-LISP"), 1181("FORMAT", "ACL2-USER", "COMMON-LISP"), 1182("HASH-TABLE-TEST", "ACL2-USER", "COMMON-LISP"), 1183("FORMATTER", "ACL2-USER", "COMMON-LISP"), 1184("HOST-NAMESTRING", "ACL2-USER", "COMMON-LISP"), 1185("FOURTH", "ACL2-USER", "COMMON-LISP"), 1186("IDENTITY", "ACL2-USER", "COMMON-LISP"), 1187("FRESH-LINE", "ACL2-USER", "COMMON-LISP"), 1188("IF", "ACL2-USER", "COMMON-LISP"), 1189("FROUND", "ACL2-USER", "COMMON-LISP"), 1190("IGNORABLE", "ACL2-USER", "COMMON-LISP"), 1191("FTRUNCATE", "ACL2-USER", "COMMON-LISP"), 1192("IGNORE", "ACL2-USER", "COMMON-LISP"), 1193("FTYPE", "ACL2-USER", "COMMON-LISP"), 1194("IGNORE-ERRORS", "ACL2-USER", "COMMON-LISP"), 1195("FUNCALL", "ACL2-USER", "COMMON-LISP"), 1196("IMAGPART", "ACL2-USER", "COMMON-LISP"), 1197("FUNCTION", "ACL2-USER", "COMMON-LISP"), 1198("IMPORT", "ACL2-USER", "COMMON-LISP"), 1199("FUNCTION-KEYWORDS", "ACL2-USER", "COMMON-LISP"), 1200("IN-PACKAGE", "ACL2-USER", "COMMON-LISP"), 1201("FUNCTION-LAMBDA-EXPRESSION", "ACL2-USER", "COMMON-LISP"), 1202("INCF", "ACL2-USER", "COMMON-LISP"), 1203("FUNCTIONP", "ACL2-USER", "COMMON-LISP"), 1204("INITIALIZE-INSTANCE", "ACL2-USER", "COMMON-LISP"), 1205("GCD", "ACL2-USER", "COMMON-LISP"), 1206("INLINE", "ACL2-USER", "COMMON-LISP"), 1207("GENERIC-FUNCTION", "ACL2-USER", "COMMON-LISP"), 1208("INPUT-STREAM-P", "ACL2-USER", "COMMON-LISP"), 1209("GENSYM", "ACL2-USER", "COMMON-LISP"), 1210("INSPECT", "ACL2-USER", "COMMON-LISP"), 1211("GENTEMP", "ACL2-USER", "COMMON-LISP"), 1212("INTEGER", "ACL2-USER", "COMMON-LISP"), 1213("GET", "ACL2-USER", "COMMON-LISP"), 1214("INTEGER-DECODE-FLOAT", "ACL2-USER", "COMMON-LISP"), 1215("GET-DECODED-TIME", "ACL2-USER", "COMMON-LISP"), 1216("INTEGER-LENGTH", "ACL2-USER", "COMMON-LISP"), 1217("GET-DISPATCH-MACRO-CHARACTER", "ACL2-USER", "COMMON-LISP"), 1218("INTEGERP", "ACL2-USER", "COMMON-LISP"), 1219("GET-INTERNAL-REAL-TIME", "ACL2-USER", "COMMON-LISP"), 1220("INTERACTIVE-STREAM-P", "ACL2-USER", "COMMON-LISP"), 1221("INTERN", "ACL2-USER", "COMMON-LISP"), 1222("LISP-IMPLEMENTATION-TYPE", "ACL2-USER", "COMMON-LISP"), 1223("INTERNAL-TIME-UNITS-PER-SECOND", "ACL2-USER", "COMMON-LISP"), 1224("LISP-IMPLEMENTATION-VERSION", "ACL2-USER", "COMMON-LISP"), 1225("INTERSECTION", "ACL2-USER", "COMMON-LISP"), 1226("LIST", "ACL2-USER", "COMMON-LISP"), 1227("INVALID-METHOD-ERROR", "ACL2-USER", "COMMON-LISP"), 1228("LIST*", "ACL2-USER", "COMMON-LISP"), 1229("INVOKE-DEBUGGER", "ACL2-USER", "COMMON-LISP"), 1230("LIST-ALL-PACKAGES", "ACL2-USER", "COMMON-LISP"), 1231("INVOKE-RESTART", "ACL2-USER", "COMMON-LISP"), 1232("LIST-LENGTH", "ACL2-USER", "COMMON-LISP"), 1233("INVOKE-RESTART-INTERACTIVELY", "ACL2-USER", "COMMON-LISP"), 1234("LISTEN", "ACL2-USER", "COMMON-LISP"), 1235("ISQRT", "ACL2-USER", "COMMON-LISP"), 1236("LISTP", "ACL2-USER", "COMMON-LISP"), 1237("KEYWORD", "ACL2-USER", "COMMON-LISP"), 1238("LOAD", "ACL2-USER", "COMMON-LISP"), 1239("KEYWORDP", "ACL2-USER", "COMMON-LISP"), 1240("LOAD-LOGICAL-PATHNAME-TRANSLATIONS", "ACL2-USER", "COMMON-LISP"), 1241("LABELS", "ACL2-USER", "COMMON-LISP"), 1242("LOAD-TIME-VALUE", "ACL2-USER", "COMMON-LISP"), 1243("LAMBDA", "ACL2-USER", "COMMON-LISP"), 1244("LOCALLY", "ACL2-USER", "COMMON-LISP"), 1245("LAMBDA-LIST-KEYWORDS", "ACL2-USER", "COMMON-LISP"), 1246("LOG", "ACL2-USER", "COMMON-LISP"), 1247("LAMBDA-PARAMETERS-LIMIT", "ACL2-USER", "COMMON-LISP"), 1248("LOGAND", "ACL2-USER", "COMMON-LISP"), 1249("LAST", "ACL2-USER", "COMMON-LISP"), 1250("LOGANDC1", "ACL2-USER", "COMMON-LISP"), 1251("LCM", "ACL2-USER", "COMMON-LISP"), 1252("LOGANDC2", "ACL2-USER", "COMMON-LISP"), 1253("LDB", "ACL2-USER", "COMMON-LISP"), 1254("LOGBITP", "ACL2-USER", "COMMON-LISP"), 1255("LDB-TEST", "ACL2-USER", "COMMON-LISP"), 1256("LOGCOUNT", "ACL2-USER", "COMMON-LISP"), 1257("LDIFF", "ACL2-USER", "COMMON-LISP"), 1258("LOGEQV", "ACL2-USER", "COMMON-LISP"), 1259("LEAST-NEGATIVE-DOUBLE-FLOAT", "ACL2-USER", "COMMON-LISP"), 1260("LOGICAL-PATHNAME", "ACL2-USER", "COMMON-LISP"), 1261("LEAST-NEGATIVE-LONG-FLOAT", "ACL2-USER", "COMMON-LISP"), 1262("LOGICAL-PATHNAME-TRANSLATIONS", "ACL2-USER", "COMMON-LISP"), 1263("LEAST-NEGATIVE-NORMALIZED-DOUBLE-FLOAT", "ACL2-USER", "COMMON-LISP"), 1264("LOGIOR", "ACL2-USER", "COMMON-LISP"), 1265("LEAST-NEGATIVE-NORMALIZED-LONG-FLOAT", "ACL2-USER", "COMMON-LISP"), 1266("LOGNAND", "ACL2-USER", "COMMON-LISP"), 1267("LEAST-NEGATIVE-NORMALIZED-SHORT-FLOAT", "ACL2-USER", "COMMON-LISP"), 1268("LOGNOR", "ACL2-USER", "COMMON-LISP"), 1269("LEAST-NEGATIVE-NORMALIZED-SINGLE-FLOAT", "ACL2-USER", "COMMON-LISP"), 1270("LOGNOT", "ACL2-USER", "COMMON-LISP"), 1271("LEAST-NEGATIVE-SHORT-FLOAT", "ACL2-USER", "COMMON-LISP"), 1272("LOGORC1", "ACL2-USER", "COMMON-LISP"), 1273("LEAST-NEGATIVE-SINGLE-FLOAT", "ACL2-USER", "COMMON-LISP"), 1274("LOGORC2", "ACL2-USER", "COMMON-LISP"), 1275("LEAST-POSITIVE-DOUBLE-FLOAT", "ACL2-USER", "COMMON-LISP"), 1276("LOGTEST", "ACL2-USER", "COMMON-LISP"), 1277("LEAST-POSITIVE-LONG-FLOAT", "ACL2-USER", "COMMON-LISP"), 1278("LOGXOR", "ACL2-USER", "COMMON-LISP"), 1279("LEAST-POSITIVE-NORMALIZED-DOUBLE-FLOAT", "ACL2-USER", "COMMON-LISP"), 1280("LONG-FLOAT", "ACL2-USER", "COMMON-LISP"), 1281("LEAST-POSITIVE-NORMALIZED-LONG-FLOAT", "ACL2-USER", "COMMON-LISP"), 1282("LONG-FLOAT-EPSILON", "ACL2-USER", "COMMON-LISP"), 1283("LEAST-POSITIVE-NORMALIZED-SHORT-FLOAT", "ACL2-USER", "COMMON-LISP"), 1284("LONG-FLOAT-NEGATIVE-EPSILON", "ACL2-USER", "COMMON-LISP"), 1285("LEAST-POSITIVE-NORMALIZED-SINGLE-FLOAT", "ACL2-USER", "COMMON-LISP"), 1286("LONG-SITE-NAME", "ACL2-USER", "COMMON-LISP"), 1287("LEAST-POSITIVE-SHORT-FLOAT", "ACL2-USER", "COMMON-LISP"), 1288("LOOP", "ACL2-USER", "COMMON-LISP"), 1289("LEAST-POSITIVE-SINGLE-FLOAT", "ACL2-USER", "COMMON-LISP"), 1290("LOOP-FINISH", "ACL2-USER", "COMMON-LISP"), 1291("LENGTH", "ACL2-USER", "COMMON-LISP"), 1292("LOWER-CASE-P", "ACL2-USER", "COMMON-LISP"), 1293("LET", "ACL2-USER", "COMMON-LISP"), 1294("MACHINE-INSTANCE", "ACL2-USER", "COMMON-LISP"), 1295("LET*", "ACL2-USER", "COMMON-LISP"), 1296("MACHINE-TYPE", "ACL2-USER", "COMMON-LISP"), 1297("MACHINE-VERSION", "ACL2-USER", "COMMON-LISP"), 1298("MASK-FIELD", "ACL2-USER", "COMMON-LISP"), 1299("MACRO-FUNCTION", "ACL2-USER", "COMMON-LISP"), 1300("MAX", "ACL2-USER", "COMMON-LISP"), 1301("MACROEXPAND", "ACL2-USER", "COMMON-LISP"), 1302("MEMBER", "ACL2-USER", "COMMON-LISP"), 1303("MACROEXPAND-1", "ACL2-USER", "COMMON-LISP"), 1304("MEMBER-IF", "ACL2-USER", "COMMON-LISP"), 1305("MACROLET", "ACL2-USER", "COMMON-LISP"), 1306("MEMBER-IF-NOT", "ACL2-USER", "COMMON-LISP"), 1307("MAKE-ARRAY", "ACL2-USER", "COMMON-LISP"), 1308("MERGE", "ACL2-USER", "COMMON-LISP"), 1309("MAKE-BROADCAST-STREAM", "ACL2-USER", "COMMON-LISP"), 1310("MERGE-PATHNAMES", "ACL2-USER", "COMMON-LISP"), 1311("MAKE-CONCATENATED-STREAM", "ACL2-USER", "COMMON-LISP"), 1312("METHOD", "ACL2-USER", "COMMON-LISP"), 1313("MAKE-CONDITION", "ACL2-USER", "COMMON-LISP"), 1314("METHOD-COMBINATION", "ACL2-USER", "COMMON-LISP"), 1315("MAKE-DISPATCH-MACRO-CHARACTER", "ACL2-USER", "COMMON-LISP"), 1316("METHOD-COMBINATION-ERROR", "ACL2-USER", "COMMON-LISP"), 1317("MAKE-ECHO-STREAM", "ACL2-USER", "COMMON-LISP"), 1318("METHOD-QUALIFIERS", "ACL2-USER", "COMMON-LISP"), 1319("MAKE-HASH-TABLE", "ACL2-USER", "COMMON-LISP"), 1320("MIN", "ACL2-USER", "COMMON-LISP"), 1321("MAKE-INSTANCE", "ACL2-USER", "COMMON-LISP"), 1322("MINUSP", "ACL2-USER", "COMMON-LISP"), 1323("MAKE-INSTANCES-OBSOLETE", "ACL2-USER", "COMMON-LISP"), 1324("MISMATCH", "ACL2-USER", "COMMON-LISP"), 1325("MAKE-LIST", "ACL2-USER", "COMMON-LISP"), 1326("MOD", "ACL2-USER", "COMMON-LISP"), 1327("MAKE-LOAD-FORM", "ACL2-USER", "COMMON-LISP"), 1328("MOST-NEGATIVE-DOUBLE-FLOAT", "ACL2-USER", "COMMON-LISP"), 1329("MAKE-LOAD-FORM-SAVING-SLOTS", "ACL2-USER", "COMMON-LISP"), 1330("MOST-NEGATIVE-FIXNUM", "ACL2-USER", "COMMON-LISP"), 1331("MAKE-METHOD", "ACL2-USER", "COMMON-LISP"), 1332("MOST-NEGATIVE-LONG-FLOAT", "ACL2-USER", "COMMON-LISP"), 1333("MAKE-PACKAGE", "ACL2-USER", "COMMON-LISP"), 1334("MOST-NEGATIVE-SHORT-FLOAT", "ACL2-USER", "COMMON-LISP"), 1335("MAKE-PATHNAME", "ACL2-USER", "COMMON-LISP"), 1336("MOST-NEGATIVE-SINGLE-FLOAT", "ACL2-USER", "COMMON-LISP"), 1337("MAKE-RANDOM-STATE", "ACL2-USER", "COMMON-LISP"), 1338("MOST-POSITIVE-DOUBLE-FLOAT", "ACL2-USER", "COMMON-LISP"), 1339("MAKE-SEQUENCE", "ACL2-USER", "COMMON-LISP"), 1340("MOST-POSITIVE-FIXNUM", "ACL2-USER", "COMMON-LISP"), 1341("MAKE-STRING", "ACL2-USER", "COMMON-LISP"), 1342("MOST-POSITIVE-LONG-FLOAT", "ACL2-USER", "COMMON-LISP"), 1343("MAKE-STRING-INPUT-STREAM", "ACL2-USER", "COMMON-LISP"), 1344("MOST-POSITIVE-SHORT-FLOAT", "ACL2-USER", "COMMON-LISP"), 1345("MAKE-STRING-OUTPUT-STREAM", "ACL2-USER", "COMMON-LISP"), 1346("MOST-POSITIVE-SINGLE-FLOAT", "ACL2-USER", "COMMON-LISP"), 1347("MAKE-SYMBOL", "ACL2-USER", "COMMON-LISP"), 1348("MUFFLE-WARNING", "ACL2-USER", "COMMON-LISP"), 1349("MAKE-SYNONYM-STREAM", "ACL2-USER", "COMMON-LISP"), 1350("MULTIPLE-VALUE-BIND", "ACL2-USER", "COMMON-LISP"), 1351("MAKE-TWO-WAY-STREAM", "ACL2-USER", "COMMON-LISP"), 1352("MULTIPLE-VALUE-CALL", "ACL2-USER", "COMMON-LISP"), 1353("MAKUNBOUND", "ACL2-USER", "COMMON-LISP"), 1354("MULTIPLE-VALUE-LIST", "ACL2-USER", "COMMON-LISP"), 1355("MAP", "ACL2-USER", "COMMON-LISP"), 1356("MULTIPLE-VALUE-PROG1", "ACL2-USER", "COMMON-LISP"), 1357("MAP-INTO", "ACL2-USER", "COMMON-LISP"), 1358("MULTIPLE-VALUE-SETQ", "ACL2-USER", "COMMON-LISP"), 1359("MAPC", "ACL2-USER", "COMMON-LISP"), 1360("MULTIPLE-VALUES-LIMIT", "ACL2-USER", "COMMON-LISP"), 1361("MAPCAN", "ACL2-USER", "COMMON-LISP"), 1362("NAME-CHAR", "ACL2-USER", "COMMON-LISP"), 1363("MAPCAR", "ACL2-USER", "COMMON-LISP"), 1364("NAMESTRING", "ACL2-USER", "COMMON-LISP"), 1365("MAPCON", "ACL2-USER", "COMMON-LISP"), 1366("NBUTLAST", "ACL2-USER", "COMMON-LISP"), 1367("MAPHASH", "ACL2-USER", "COMMON-LISP"), 1368("NCONC", "ACL2-USER", "COMMON-LISP"), 1369("MAPL", "ACL2-USER", "COMMON-LISP"), 1370("NEXT-METHOD-P", "ACL2-USER", "COMMON-LISP"), 1371("MAPLIST", "ACL2-USER", "COMMON-LISP"), 1372("NIL", "ACL2-USER", "COMMON-LISP"), 1373("NINTERSECTION", "ACL2-USER", "COMMON-LISP"), 1374("PACKAGE-ERROR", "ACL2-USER", "COMMON-LISP"), 1375("NINTH", "ACL2-USER", "COMMON-LISP"), 1376("PACKAGE-ERROR-PACKAGE", "ACL2-USER", "COMMON-LISP"), 1377("NO-APPLICABLE-METHOD", "ACL2-USER", "COMMON-LISP"), 1378("PACKAGE-NAME", "ACL2-USER", "COMMON-LISP"), 1379("NO-NEXT-METHOD", "ACL2-USER", "COMMON-LISP"), 1380("PACKAGE-NICKNAMES", "ACL2-USER", "COMMON-LISP"), 1381("NOT", "ACL2-USER", "COMMON-LISP"), 1382("PACKAGE-SHADOWING-SYMBOLS", "ACL2-USER", "COMMON-LISP"), 1383("NOTANY", "ACL2-USER", "COMMON-LISP"), 1384("PACKAGE-USE-LIST", "ACL2-USER", "COMMON-LISP"), 1385("NOTEVERY", "ACL2-USER", "COMMON-LISP"), 1386("PACKAGE-USED-BY-LIST", "ACL2-USER", "COMMON-LISP"), 1387("NOTINLINE", "ACL2-USER", "COMMON-LISP"), 1388("PACKAGEP", "ACL2-USER", "COMMON-LISP"), 1389("NRECONC", "ACL2-USER", "COMMON-LISP"), 1390("PAIRLIS", "ACL2-USER", "COMMON-LISP"), 1391("NREVERSE", "ACL2-USER", "COMMON-LISP"), 1392("PARSE-ERROR", "ACL2-USER", "COMMON-LISP"), 1393("NSET-DIFFERENCE", "ACL2-USER", "COMMON-LISP"), 1394("PARSE-INTEGER", "ACL2-USER", "COMMON-LISP"), 1395("NSET-EXCLUSIVE-OR", "ACL2-USER", "COMMON-LISP"), 1396("PARSE-NAMESTRING", "ACL2-USER", "COMMON-LISP"), 1397("NSTRING-CAPITALIZE", "ACL2-USER", "COMMON-LISP"), 1398("PATHNAME", "ACL2-USER", "COMMON-LISP"), 1399("NSTRING-DOWNCASE", "ACL2-USER", "COMMON-LISP"), 1400("PATHNAME-DEVICE", "ACL2-USER", "COMMON-LISP"), 1401("NSTRING-UPCASE", "ACL2-USER", "COMMON-LISP"), 1402("PATHNAME-DIRECTORY", "ACL2-USER", "COMMON-LISP"), 1403("NSUBLIS", "ACL2-USER", "COMMON-LISP"), 1404("PATHNAME-HOST", "ACL2-USER", "COMMON-LISP"), 1405("NSUBST", "ACL2-USER", "COMMON-LISP"), 1406("PATHNAME-MATCH-P", "ACL2-USER", "COMMON-LISP"), 1407("NSUBST-IF", "ACL2-USER", "COMMON-LISP"), 1408("PATHNAME-NAME", "ACL2-USER", "COMMON-LISP"), 1409("NSUBST-IF-NOT", "ACL2-USER", "COMMON-LISP"), 1410("PATHNAME-TYPE", "ACL2-USER", "COMMON-LISP"), 1411("NSUBSTITUTE", "ACL2-USER", "COMMON-LISP"), 1412("PATHNAME-VERSION", "ACL2-USER", "COMMON-LISP"), 1413("NSUBSTITUTE-IF", "ACL2-USER", "COMMON-LISP"), 1414("PATHNAMEP", "ACL2-USER", "COMMON-LISP"), 1415("NSUBSTITUTE-IF-NOT", "ACL2-USER", "COMMON-LISP"), 1416("PEEK-CHAR", "ACL2-USER", "COMMON-LISP"), 1417("NTH", "ACL2-USER", "COMMON-LISP"), 1418("PHASE", "ACL2-USER", "COMMON-LISP"), 1419("NTH-VALUE", "ACL2-USER", "COMMON-LISP"), 1420("PI", "ACL2-USER", "COMMON-LISP"), 1421("NTHCDR", "ACL2-USER", "COMMON-LISP"), 1422("PLUSP", "ACL2-USER", "COMMON-LISP"), 1423("NULL", "ACL2-USER", "COMMON-LISP"), 1424("POP", "ACL2-USER", "COMMON-LISP"), 1425("NUMBER", "ACL2-USER", "COMMON-LISP"), 1426("POSITION", "ACL2-USER", "COMMON-LISP"), 1427("NUMBERP", "ACL2-USER", "COMMON-LISP"), 1428("POSITION-IF", "ACL2-USER", "COMMON-LISP"), 1429("NUMERATOR", "ACL2-USER", "COMMON-LISP"), 1430("POSITION-IF-NOT", "ACL2-USER", "COMMON-LISP"), 1431("NUNION", "ACL2-USER", "COMMON-LISP"), 1432("PPRINT", "ACL2-USER", "COMMON-LISP"), 1433("ODDP", "ACL2-USER", "COMMON-LISP"), 1434("PPRINT-DISPATCH", "ACL2-USER", "COMMON-LISP"), 1435("OPEN", "ACL2-USER", "COMMON-LISP"), 1436("PPRINT-EXIT-IF-LIST-EXHAUSTED", "ACL2-USER", "COMMON-LISP"), 1437("OPEN-STREAM-P", "ACL2-USER", "COMMON-LISP"), 1438("PPRINT-FILL", "ACL2-USER", "COMMON-LISP"), 1439("OPTIMIZE", "ACL2-USER", "COMMON-LISP"), 1440("PPRINT-INDENT", "ACL2-USER", "COMMON-LISP"), 1441("OR", "ACL2-USER", "COMMON-LISP"), 1442("PPRINT-LINEAR", "ACL2-USER", "COMMON-LISP"), 1443("OTHERWISE", "ACL2-USER", "COMMON-LISP"), 1444("PPRINT-LOGICAL-BLOCK", "ACL2-USER", "COMMON-LISP"), 1445("OUTPUT-STREAM-P", "ACL2-USER", "COMMON-LISP"), 1446("PPRINT-NEWLINE", "ACL2-USER", "COMMON-LISP"), 1447("PACKAGE", "ACL2-USER", "COMMON-LISP"), 1448("PPRINT-POP", "ACL2-USER", "COMMON-LISP"), 1449("PPRINT-TAB", "ACL2-USER", "COMMON-LISP"), 1450("READ-CHAR", "ACL2-USER", "COMMON-LISP"), 1451("PPRINT-TABULAR", "ACL2-USER", "COMMON-LISP"), 1452("READ-CHAR-NO-HANG", "ACL2-USER", "COMMON-LISP"), 1453("PRIN1", "ACL2-USER", "COMMON-LISP"), 1454("READ-DELIMITED-LIST", "ACL2-USER", "COMMON-LISP"), 1455("PRIN1-TO-STRING", "ACL2-USER", "COMMON-LISP"), 1456("READ-FROM-STRING", "ACL2-USER", "COMMON-LISP"), 1457("PRINC", "ACL2-USER", "COMMON-LISP"), 1458("READ-LINE", "ACL2-USER", "COMMON-LISP"), 1459("PRINC-TO-STRING", "ACL2-USER", "COMMON-LISP"), 1460("READ-PRESERVING-WHITESPACE", "ACL2-USER", "COMMON-LISP"), 1461("PRINT", "ACL2-USER", "COMMON-LISP"), 1462("READ-SEQUENCE", "ACL2-USER", "COMMON-LISP"), 1463("PRINT-NOT-READABLE", "ACL2-USER", "COMMON-LISP"), 1464("READER-ERROR", "ACL2-USER", "COMMON-LISP"), 1465("PRINT-NOT-READABLE-OBJECT", "ACL2-USER", "COMMON-LISP"), 1466("READTABLE", "ACL2-USER", "COMMON-LISP"), 1467("PRINT-OBJECT", "ACL2-USER", "COMMON-LISP"), 1468("READTABLE-CASE", "ACL2-USER", "COMMON-LISP"), 1469("PRINT-UNREADABLE-OBJECT", "ACL2-USER", "COMMON-LISP"), 1470("READTABLEP", "ACL2-USER", "COMMON-LISP"), 1471("PROBE-FILE", "ACL2-USER", "COMMON-LISP"), 1472("REAL", "ACL2-USER", "COMMON-LISP"), 1473("PROCLAIM", "ACL2-USER", "COMMON-LISP"), 1474("REALP", "ACL2-USER", "COMMON-LISP"), 1475("PROG", "ACL2-USER", "COMMON-LISP"), 1476("REALPART", "ACL2-USER", "COMMON-LISP"), 1477("PROG*", "ACL2-USER", "COMMON-LISP"), 1478("REDUCE", "ACL2-USER", "COMMON-LISP"), 1479("PROG1", "ACL2-USER", "COMMON-LISP"), 1480("REINITIALIZE-INSTANCE", "ACL2-USER", "COMMON-LISP"), 1481("PROG2", "ACL2-USER", "COMMON-LISP"), 1482("REM", "ACL2-USER", "COMMON-LISP"), 1483("PROGN", "ACL2-USER", "COMMON-LISP"), 1484("REMF", "ACL2-USER", "COMMON-LISP"), 1485("PROGRAM-ERROR", "ACL2-USER", "COMMON-LISP"), 1486("REMHASH", "ACL2-USER", "COMMON-LISP"), 1487("PROGV", "ACL2-USER", "COMMON-LISP"), 1488("REMOVE", "ACL2-USER", "COMMON-LISP"), 1489("PROVIDE", "ACL2-USER", "COMMON-LISP"), 1490("REMOVE-DUPLICATES", "ACL2-USER", "COMMON-LISP"), 1491("PSETF", "ACL2-USER", "COMMON-LISP"), 1492("REMOVE-IF", "ACL2-USER", "COMMON-LISP"), 1493("PSETQ", "ACL2-USER", "COMMON-LISP"), 1494("REMOVE-IF-NOT", "ACL2-USER", "COMMON-LISP"), 1495("PUSH", "ACL2-USER", "COMMON-LISP"), 1496("REMOVE-METHOD", "ACL2-USER", "COMMON-LISP"), 1497("PUSHNEW", "ACL2-USER", "COMMON-LISP"), 1498("REMPROP", "ACL2-USER", "COMMON-LISP"), 1499("QUOTE", "ACL2-USER", "COMMON-LISP"), 1500("RENAME-FILE", "ACL2-USER", "COMMON-LISP"), 1501("RANDOM", "ACL2-USER", "COMMON-LISP"), 1502("RENAME-PACKAGE", "ACL2-USER", "COMMON-LISP"), 1503("RANDOM-STATE", "ACL2-USER", "COMMON-LISP"), 1504("REPLACE", "ACL2-USER", "COMMON-LISP"), 1505("RANDOM-STATE-P", "ACL2-USER", "COMMON-LISP"), 1506("REQUIRE", "ACL2-USER", "COMMON-LISP"), 1507("RASSOC", "ACL2-USER", "COMMON-LISP"), 1508("REST", "ACL2-USER", "COMMON-LISP"), 1509("RASSOC-IF", "ACL2-USER", "COMMON-LISP"), 1510("RESTART", "ACL2-USER", "COMMON-LISP"), 1511("RASSOC-IF-NOT", "ACL2-USER", "COMMON-LISP"), 1512("RESTART-BIND", "ACL2-USER", "COMMON-LISP"), 1513("RATIO", "ACL2-USER", "COMMON-LISP"), 1514("RESTART-CASE", "ACL2-USER", "COMMON-LISP"), 1515("RATIONAL", "ACL2-USER", "COMMON-LISP"), 1516("RESTART-NAME", "ACL2-USER", "COMMON-LISP"), 1517("RATIONALIZE", "ACL2-USER", "COMMON-LISP"), 1518("RETURN", "ACL2-USER", "COMMON-LISP"), 1519("RATIONALP", "ACL2-USER", "COMMON-LISP"), 1520("RETURN-FROM", "ACL2-USER", "COMMON-LISP"), 1521("READ", "ACL2-USER", "COMMON-LISP"), 1522("REVAPPEND", "ACL2-USER", "COMMON-LISP"), 1523("READ-BYTE", "ACL2-USER", "COMMON-LISP"), 1524("REVERSE", "ACL2-USER", "COMMON-LISP"), 1525("ROOM", "ACL2-USER", "COMMON-LISP"), 1526("SIMPLE-BIT-VECTOR", "ACL2-USER", "COMMON-LISP"), 1527("ROTATEF", "ACL2-USER", "COMMON-LISP"), 1528("SIMPLE-BIT-VECTOR-P", "ACL2-USER", "COMMON-LISP"), 1529("ROUND", "ACL2-USER", "COMMON-LISP"), 1530("SIMPLE-CONDITION", "ACL2-USER", "COMMON-LISP"), 1531("ROW-MAJOR-AREF", "ACL2-USER", "COMMON-LISP"), 1532("SIMPLE-CONDITION-FORMAT-ARGUMENTS", "ACL2-USER", "COMMON-LISP"), 1533("RPLACA", "ACL2-USER", "COMMON-LISP"), 1534("SIMPLE-CONDITION-FORMAT-CONTROL", "ACL2-USER", "COMMON-LISP"), 1535("RPLACD", "ACL2-USER", "COMMON-LISP"), 1536("SIMPLE-ERROR", "ACL2-USER", "COMMON-LISP"), 1537("SAFETY", "ACL2-USER", "COMMON-LISP"), 1538("SIMPLE-STRING", "ACL2-USER", "COMMON-LISP"), 1539("SATISFIES", "ACL2-USER", "COMMON-LISP"), 1540("SIMPLE-STRING-P", "ACL2-USER", "COMMON-LISP"), 1541("SBIT", "ACL2-USER", "COMMON-LISP"), 1542("SIMPLE-TYPE-ERROR", "ACL2-USER", "COMMON-LISP"), 1543("SCALE-FLOAT", "ACL2-USER", "COMMON-LISP"), 1544("SIMPLE-VECTOR", "ACL2-USER", "COMMON-LISP"), 1545("SCHAR", "ACL2-USER", "COMMON-LISP"), 1546("SIMPLE-VECTOR-P", "ACL2-USER", "COMMON-LISP"), 1547("SEARCH", "ACL2-USER", "COMMON-LISP"), 1548("SIMPLE-WARNING", "ACL2-USER", "COMMON-LISP"), 1549("SECOND", "ACL2-USER", "COMMON-LISP"), 1550("SIN", "ACL2-USER", "COMMON-LISP"), 1551("SEQUENCE", "ACL2-USER", "COMMON-LISP"), 1552("SINGLE-FLOAT", "ACL2-USER", "COMMON-LISP"), 1553("SERIOUS-CONDITION", "ACL2-USER", "COMMON-LISP"), 1554("SINGLE-FLOAT-EPSILON", "ACL2-USER", "COMMON-LISP"), 1555("SET", "ACL2-USER", "COMMON-LISP"), 1556("SINGLE-FLOAT-NEGATIVE-EPSILON", "ACL2-USER", "COMMON-LISP"), 1557("SET-DIFFERENCE", "ACL2-USER", "COMMON-LISP"), 1558("SINH", "ACL2-USER", "COMMON-LISP"), 1559("SET-DISPATCH-MACRO-CHARACTER", "ACL2-USER", "COMMON-LISP"), 1560("SIXTH", "ACL2-USER", "COMMON-LISP"), 1561("SET-EXCLUSIVE-OR", "ACL2-USER", "COMMON-LISP"), 1562("SLEEP", "ACL2-USER", "COMMON-LISP"), 1563("SET-MACRO-CHARACTER", "ACL2-USER", "COMMON-LISP"), 1564("SLOT-BOUNDP", "ACL2-USER", "COMMON-LISP"), 1565("SET-PPRINT-DISPATCH", "ACL2-USER", "COMMON-LISP"), 1566("SLOT-EXISTS-P", "ACL2-USER", "COMMON-LISP"), 1567("SET-SYNTAX-FROM-CHAR", "ACL2-USER", "COMMON-LISP"), 1568("SLOT-MAKUNBOUND", "ACL2-USER", "COMMON-LISP"), 1569("SETF", "ACL2-USER", "COMMON-LISP"), 1570("SLOT-MISSING", "ACL2-USER", "COMMON-LISP"), 1571("SETQ", "ACL2-USER", "COMMON-LISP"), 1572("SLOT-UNBOUND", "ACL2-USER", "COMMON-LISP"), 1573("SEVENTH", "ACL2-USER", "COMMON-LISP"), 1574("SLOT-VALUE", "ACL2-USER", "COMMON-LISP"), 1575("SHADOW", "ACL2-USER", "COMMON-LISP"), 1576("SOFTWARE-TYPE", "ACL2-USER", "COMMON-LISP"), 1577("SHADOWING-IMPORT", "ACL2-USER", "COMMON-LISP"), 1578("SOFTWARE-VERSION", "ACL2-USER", "COMMON-LISP"), 1579("SHARED-INITIALIZE", "ACL2-USER", "COMMON-LISP"), 1580("SOME", "ACL2-USER", "COMMON-LISP"), 1581("SHIFTF", "ACL2-USER", "COMMON-LISP"), 1582("SORT", "ACL2-USER", "COMMON-LISP"), 1583("SHORT-FLOAT", "ACL2-USER", "COMMON-LISP"), 1584("SPACE", "ACL2-USER", "COMMON-LISP"), 1585("SHORT-FLOAT-EPSILON", "ACL2-USER", "COMMON-LISP"), 1586("SPECIAL", "ACL2-USER", "COMMON-LISP"), 1587("SHORT-FLOAT-NEGATIVE-EPSILON", "ACL2-USER", "COMMON-LISP"), 1588("SPECIAL-OPERATOR-P", "ACL2-USER", "COMMON-LISP"), 1589("SHORT-SITE-NAME", "ACL2-USER", "COMMON-LISP"), 1590("SPEED", "ACL2-USER", "COMMON-LISP"), 1591("SIGNAL", "ACL2-USER", "COMMON-LISP"), 1592("SQRT", "ACL2-USER", "COMMON-LISP"), 1593("SIGNED-BYTE", "ACL2-USER", "COMMON-LISP"), 1594("STABLE-SORT", "ACL2-USER", "COMMON-LISP"), 1595("SIGNUM", "ACL2-USER", "COMMON-LISP"), 1596("STANDARD", "ACL2-USER", "COMMON-LISP"), 1597("SIMPLE-ARRAY", "ACL2-USER", "COMMON-LISP"), 1598("STANDARD-CHAR", "ACL2-USER", "COMMON-LISP"), 1599("SIMPLE-BASE-STRING", "ACL2-USER", "COMMON-LISP"), 1600("STANDARD-CHAR-P", "ACL2-USER", "COMMON-LISP"), 1601("STANDARD-CLASS", "ACL2-USER", "COMMON-LISP"), 1602("SUBLIS", "ACL2-USER", "COMMON-LISP"), 1603("STANDARD-GENERIC-FUNCTION", "ACL2-USER", "COMMON-LISP"), 1604("SUBSEQ", "ACL2-USER", "COMMON-LISP"), 1605("STANDARD-METHOD", "ACL2-USER", "COMMON-LISP"), 1606("SUBSETP", "ACL2-USER", "COMMON-LISP"), 1607("STANDARD-OBJECT", "ACL2-USER", "COMMON-LISP"), 1608("SUBST", "ACL2-USER", "COMMON-LISP"), 1609("STEP", "ACL2-USER", "COMMON-LISP"), 1610("SUBST-IF", "ACL2-USER", "COMMON-LISP"), 1611("STORAGE-CONDITION", "ACL2-USER", "COMMON-LISP"), 1612("SUBST-IF-NOT", "ACL2-USER", "COMMON-LISP"), 1613("STORE-VALUE", "ACL2-USER", "COMMON-LISP"), 1614("SUBSTITUTE", "ACL2-USER", "COMMON-LISP"), 1615("STREAM", "ACL2-USER", "COMMON-LISP"), 1616("SUBSTITUTE-IF", "ACL2-USER", "COMMON-LISP"), 1617("STREAM-ELEMENT-TYPE", "ACL2-USER", "COMMON-LISP"), 1618("SUBSTITUTE-IF-NOT", "ACL2-USER", "COMMON-LISP"), 1619("STREAM-ERROR", "ACL2-USER", "COMMON-LISP"), 1620("SUBTYPEP", "ACL2-USER", "COMMON-LISP"), 1621("STREAM-ERROR-STREAM", "ACL2-USER", "COMMON-LISP"), 1622("SVREF", "ACL2-USER", "COMMON-LISP"), 1623("STREAM-EXTERNAL-FORMAT", "ACL2-USER", "COMMON-LISP"), 1624("SXHASH", "ACL2-USER", "COMMON-LISP"), 1625("STREAMP", "ACL2-USER", "COMMON-LISP"), 1626("SYMBOL", "ACL2-USER", "COMMON-LISP"), 1627("STRING", "ACL2-USER", "COMMON-LISP"), 1628("SYMBOL-FUNCTION", "ACL2-USER", "COMMON-LISP"), 1629("STRING-CAPITALIZE", "ACL2-USER", "COMMON-LISP"), 1630("SYMBOL-MACROLET", "ACL2-USER", "COMMON-LISP"), 1631("STRING-DOWNCASE", "ACL2-USER", "COMMON-LISP"), 1632("SYMBOL-NAME", "ACL2-USER", "COMMON-LISP"), 1633("STRING-EQUAL", "ACL2-USER", "COMMON-LISP"), 1634("SYMBOL-PACKAGE", "ACL2-USER", "COMMON-LISP"), 1635("STRING-GREATERP", "ACL2-USER", "COMMON-LISP"), 1636("SYMBOL-PLIST", "ACL2-USER", "COMMON-LISP"), 1637("STRING-LEFT-TRIM", "ACL2-USER", "COMMON-LISP"), 1638("SYMBOL-VALUE", "ACL2-USER", "COMMON-LISP"), 1639("STRING-LESSP", "ACL2-USER", "COMMON-LISP"), 1640("SYMBOLP", "ACL2-USER", "COMMON-LISP"), 1641("STRING-NOT-EQUAL", "ACL2-USER", "COMMON-LISP"), 1642("SYNONYM-STREAM", "ACL2-USER", "COMMON-LISP"), 1643("STRING-NOT-GREATERP", "ACL2-USER", "COMMON-LISP"), 1644("SYNONYM-STREAM-SYMBOL", "ACL2-USER", "COMMON-LISP"), 1645("STRING-NOT-LESSP", "ACL2-USER", "COMMON-LISP"), 1646("T", "ACL2-USER", "COMMON-LISP"), 1647("STRING-RIGHT-TRIM", "ACL2-USER", "COMMON-LISP"), 1648("TAGBODY", "ACL2-USER", "COMMON-LISP"), 1649("STRING-STREAM", "ACL2-USER", "COMMON-LISP"), 1650("TAILP", "ACL2-USER", "COMMON-LISP"), 1651("STRING-TRIM", "ACL2-USER", "COMMON-LISP"), 1652("TAN", "ACL2-USER", "COMMON-LISP"), 1653("STRING-UPCASE", "ACL2-USER", "COMMON-LISP"), 1654("TANH", "ACL2-USER", "COMMON-LISP"), 1655("STRING/=", "ACL2-USER", "COMMON-LISP"), 1656("TENTH", "ACL2-USER", "COMMON-LISP"), 1657("STRING<", "ACL2-USER", "COMMON-LISP"), 1658("TERPRI", "ACL2-USER", "COMMON-LISP"), 1659("STRING<=", "ACL2-USER", "COMMON-LISP"), 1660("THE", "ACL2-USER", "COMMON-LISP"), 1661("STRING=", "ACL2-USER", "COMMON-LISP"), 1662("THIRD", "ACL2-USER", "COMMON-LISP"), 1663("STRING>", "ACL2-USER", "COMMON-LISP"), 1664("THROW", "ACL2-USER", "COMMON-LISP"), 1665("STRING>=", "ACL2-USER", "COMMON-LISP"), 1666("TIME", "ACL2-USER", "COMMON-LISP"), 1667("STRINGP", "ACL2-USER", "COMMON-LISP"), 1668("TRACE", "ACL2-USER", "COMMON-LISP"), 1669("STRUCTURE", "ACL2-USER", "COMMON-LISP"), 1670("TRANSLATE-LOGICAL-PATHNAME", "ACL2-USER", "COMMON-LISP"), 1671("STRUCTURE-CLASS", "ACL2-USER", "COMMON-LISP"), 1672("TRANSLATE-PATHNAME", "ACL2-USER", "COMMON-LISP"), 1673("STRUCTURE-OBJECT", "ACL2-USER", "COMMON-LISP"), 1674("TREE-EQUAL", "ACL2-USER", "COMMON-LISP"), 1675("STYLE-WARNING", "ACL2-USER", "COMMON-LISP"), 1676("TRUENAME", "ACL2-USER", "COMMON-LISP"), 1677("TRUNCATE", "ACL2-USER", "COMMON-LISP"), 1678("VALUES-LIST", "ACL2-USER", "COMMON-LISP"), 1679("TWO-WAY-STREAM", "ACL2-USER", "COMMON-LISP"), 1680("VARIABLE", "ACL2-USER", "COMMON-LISP"), 1681("TWO-WAY-STREAM-INPUT-STREAM", "ACL2-USER", "COMMON-LISP"), 1682("VECTOR", "ACL2-USER", "COMMON-LISP"), 1683("TWO-WAY-STREAM-OUTPUT-STREAM", "ACL2-USER", "COMMON-LISP"), 1684("VECTOR-POP", "ACL2-USER", "COMMON-LISP"), 1685("TYPE", "ACL2-USER", "COMMON-LISP"), 1686("VECTOR-PUSH", "ACL2-USER", "COMMON-LISP"), 1687("TYPE-ERROR", "ACL2-USER", "COMMON-LISP"), 1688("VECTOR-PUSH-EXTEND", "ACL2-USER", "COMMON-LISP"), 1689("TYPE-ERROR-DATUM", "ACL2-USER", "COMMON-LISP"), 1690("VECTORP", "ACL2-USER", "COMMON-LISP"), 1691("TYPE-ERROR-EXPECTED-TYPE", "ACL2-USER", "COMMON-LISP"), 1692("WARN", "ACL2-USER", "COMMON-LISP"), 1693("TYPE-OF", "ACL2-USER", "COMMON-LISP"), 1694("WARNING", "ACL2-USER", "COMMON-LISP"), 1695("TYPECASE", "ACL2-USER", "COMMON-LISP"), 1696("WHEN", "ACL2-USER", "COMMON-LISP"), 1697("TYPEP", "ACL2-USER", "COMMON-LISP"), 1698("WILD-PATHNAME-P", "ACL2-USER", "COMMON-LISP"), 1699("UNBOUND-SLOT", "ACL2-USER", "COMMON-LISP"), 1700("WITH-ACCESSORS", "ACL2-USER", "COMMON-LISP"), 1701("UNBOUND-SLOT-INSTANCE", "ACL2-USER", "COMMON-LISP"), 1702("WITH-COMPILATION-UNIT", "ACL2-USER", "COMMON-LISP"), 1703("UNBOUND-VARIABLE", "ACL2-USER", "COMMON-LISP"), 1704("WITH-CONDITION-RESTARTS", "ACL2-USER", "COMMON-LISP"), 1705("UNDEFINED-FUNCTION", "ACL2-USER", "COMMON-LISP"), 1706("WITH-HASH-TABLE-ITERATOR", "ACL2-USER", "COMMON-LISP"), 1707("UNEXPORT", "ACL2-USER", "COMMON-LISP"), 1708("WITH-INPUT-FROM-STRING", "ACL2-USER", "COMMON-LISP"), 1709("UNINTERN", "ACL2-USER", "COMMON-LISP"), 1710("WITH-OPEN-FILE", "ACL2-USER", "COMMON-LISP"), 1711("UNION", "ACL2-USER", "COMMON-LISP"), 1712("WITH-OPEN-STREAM", "ACL2-USER", "COMMON-LISP"), 1713("UNLESS", "ACL2-USER", "COMMON-LISP"), 1714("WITH-OUTPUT-TO-STRING", "ACL2-USER", "COMMON-LISP"), 1715("UNREAD-CHAR", "ACL2-USER", "COMMON-LISP"), 1716("WITH-PACKAGE-ITERATOR", "ACL2-USER", "COMMON-LISP"), 1717("UNSIGNED-BYTE", "ACL2-USER", "COMMON-LISP"), 1718("WITH-SIMPLE-RESTART", "ACL2-USER", "COMMON-LISP"), 1719("UNTRACE", "ACL2-USER", "COMMON-LISP"), 1720("WITH-SLOTS", "ACL2-USER", "COMMON-LISP"), 1721("UNUSE-PACKAGE", "ACL2-USER", "COMMON-LISP"), 1722("WITH-STANDARD-IO-SYNTAX", "ACL2-USER", "COMMON-LISP"), 1723("UNWIND-PROTECT", "ACL2-USER", "COMMON-LISP"), 1724("WRITE", "ACL2-USER", "COMMON-LISP"), 1725("UPDATE-INSTANCE-FOR-DIFFERENT-CLASS", "ACL2-USER", "COMMON-LISP"), 1726("WRITE-BYTE", "ACL2-USER", "COMMON-LISP"), 1727("UPDATE-INSTANCE-FOR-REDEFINED-CLASS", "ACL2-USER", "COMMON-LISP"), 1728("WRITE-CHAR", "ACL2-USER", "COMMON-LISP"), 1729("UPGRADED-ARRAY-ELEMENT-TYPE", "ACL2-USER", "COMMON-LISP"), 1730("WRITE-LINE", "ACL2-USER", "COMMON-LISP"), 1731("UPGRADED-COMPLEX-PART-TYPE", "ACL2-USER", "COMMON-LISP"), 1732("WRITE-SEQUENCE", "ACL2-USER", "COMMON-LISP"), 1733("UPPER-CASE-P", "ACL2-USER", "COMMON-LISP"), 1734("WRITE-STRING", "ACL2-USER", "COMMON-LISP"), 1735("USE-PACKAGE", "ACL2-USER", "COMMON-LISP"), 1736("WRITE-TO-STRING", "ACL2-USER", "COMMON-LISP"), 1737("USE-VALUE", "ACL2-USER", "COMMON-LISP"), 1738("Y-OR-N-P", "ACL2-USER", "COMMON-LISP"), 1739("USER-HOMEDIR-PATHNAME", "ACL2-USER", "COMMON-LISP"), 1740("YES-OR-NO-P", "ACL2-USER", "COMMON-LISP"), 1741("VALUES", "ACL2-USER", "COMMON-LISP"), 1742("ZEROP", "ACL2-USER", "COMMON-LISP"), 1743("&ALLOW-OTHER-KEYS", "ACL2", "COMMON-LISP"), 1744("*PRINT-MISER-WIDTH*", "ACL2", "COMMON-LISP"), 1745("&AUX", "ACL2", "COMMON-LISP"), 1746("*PRINT-PPRINT-DISPATCH*", "ACL2", "COMMON-LISP"), 1747("&BODY", "ACL2", "COMMON-LISP"), 1748("*PRINT-PRETTY*", "ACL2", "COMMON-LISP"), 1749("&ENVIRONMENT", "ACL2", "COMMON-LISP"), 1750("*PRINT-RADIX*", "ACL2", "COMMON-LISP"), 1751("&KEY", "ACL2", "COMMON-LISP"), 1752("*PRINT-READABLY*", "ACL2", "COMMON-LISP"), 1753("&OPTIONAL", "ACL2", "COMMON-LISP"), 1754("*PRINT-RIGHT-MARGIN*", "ACL2", "COMMON-LISP"), 1755("&REST", "ACL2", "COMMON-LISP"), 1756("*QUERY-IO*", "ACL2", "COMMON-LISP"), 1757("&WHOLE", "ACL2", "COMMON-LISP"), 1758("*RANDOM-STATE*", "ACL2", "COMMON-LISP"), 1759("*", "ACL2", "COMMON-LISP"), 1760("*READ-BASE*", "ACL2", "COMMON-LISP"), 1761("**", "ACL2", "COMMON-LISP"), 1762("*READ-DEFAULT-FLOAT-FORMAT*", "ACL2", "COMMON-LISP"), 1763("***", "ACL2", "COMMON-LISP"), 1764("*READ-EVAL*", "ACL2", "COMMON-LISP"), 1765("*BREAK-ON-SIGNALS*", "ACL2", "COMMON-LISP"), 1766("*READ-SUPPRESS*", "ACL2", "COMMON-LISP"), 1767("*COMPILE-FILE-PATHNAME*", "ACL2", "COMMON-LISP"), 1768("*READTABLE*", "ACL2", "COMMON-LISP"), 1769("*COMPILE-FILE-TRUENAME*", "ACL2", "COMMON-LISP"), 1770("*STANDARD-INPUT*", "ACL2", "COMMON-LISP"), 1771("*COMPILE-PRINT*", "ACL2", "COMMON-LISP"), 1772("*STANDARD-OUTPUT*", "ACL2", "COMMON-LISP"), 1773("*COMPILE-VERBOSE*", "ACL2", "COMMON-LISP"), 1774("*TERMINAL-IO*", "ACL2", "COMMON-LISP"), 1775("*DEBUG-IO*", "ACL2", "COMMON-LISP"), 1776("*TRACE-OUTPUT*", "ACL2", "COMMON-LISP"), 1777("*DEBUGGER-HOOK*", "ACL2", "COMMON-LISP"), 1778("+", "ACL2", "COMMON-LISP"), 1779("*DEFAULT-PATHNAME-DEFAULTS*", "ACL2", "COMMON-LISP"), 1780("++", "ACL2", "COMMON-LISP"), 1781("*ERROR-OUTPUT*", "ACL2", "COMMON-LISP"), 1782("+++", "ACL2", "COMMON-LISP"), 1783("*FEATURES*", "ACL2", "COMMON-LISP"), 1784("-", "ACL2", "COMMON-LISP"), 1785("*GENSYM-COUNTER*", "ACL2", "COMMON-LISP"), 1786("/", "ACL2", "COMMON-LISP"), 1787("*LOAD-PATHNAME*", "ACL2", "COMMON-LISP"), 1788("//", "ACL2", "COMMON-LISP"), 1789("*LOAD-PRINT*", "ACL2", "COMMON-LISP"), 1790("///", "ACL2", "COMMON-LISP"), 1791("*LOAD-TRUENAME*", "ACL2", "COMMON-LISP"), 1792("/=", "ACL2", "COMMON-LISP"), 1793("*LOAD-VERBOSE*", "ACL2", "COMMON-LISP"), 1794("1+", "ACL2", "COMMON-LISP"), 1795("*MACROEXPAND-HOOK*", "ACL2", "COMMON-LISP"), 1796("1-", "ACL2", "COMMON-LISP"), 1797("*MODULES*", "ACL2", "COMMON-LISP"), 1798("<", "ACL2", "COMMON-LISP"), 1799("*PACKAGE*", "ACL2", "COMMON-LISP"), 1800("<=", "ACL2", "COMMON-LISP"), 1801("*PRINT-ARRAY*", "ACL2", "COMMON-LISP"), 1802("=", "ACL2", "COMMON-LISP"), 1803("*PRINT-BASE*", "ACL2", "COMMON-LISP"), 1804(">", "ACL2", "COMMON-LISP"), 1805("*PRINT-CASE*", "ACL2", "COMMON-LISP"), 1806(">=", "ACL2", "COMMON-LISP"), 1807("*PRINT-CIRCLE*", "ACL2", "COMMON-LISP"), 1808("ABORT", "ACL2", "COMMON-LISP"), 1809("*PRINT-ESCAPE*", "ACL2", "COMMON-LISP"), 1810("ABS", "ACL2", "COMMON-LISP"), 1811("*PRINT-GENSYM*", "ACL2", "COMMON-LISP"), 1812("ACONS", "ACL2", "COMMON-LISP"), 1813("*PRINT-LENGTH*", "ACL2", "COMMON-LISP"), 1814("ACOS", "ACL2", "COMMON-LISP"), 1815("*PRINT-LEVEL*", "ACL2", "COMMON-LISP"), 1816("ACOSH", "ACL2", "COMMON-LISP"), 1817("*PRINT-LINES*", "ACL2", "COMMON-LISP"), 1818("ADD-METHOD", "ACL2", "COMMON-LISP"), 1819("ADJOIN", "ACL2", "COMMON-LISP"), 1820("ATOM", "ACL2", "COMMON-LISP"), 1821("BOUNDP", "ACL2", "COMMON-LISP"), 1822("ADJUST-ARRAY", "ACL2", "COMMON-LISP"), 1823("BASE-CHAR", "ACL2", "COMMON-LISP"), 1824("BREAK", "ACL2", "COMMON-LISP"), 1825("ADJUSTABLE-ARRAY-P", "ACL2", "COMMON-LISP"), 1826("BASE-STRING", "ACL2", "COMMON-LISP"), 1827("BROADCAST-STREAM", "ACL2", "COMMON-LISP"), 1828("ALLOCATE-INSTANCE", "ACL2", "COMMON-LISP"), 1829("BIGNUM", "ACL2", "COMMON-LISP"), 1830("BROADCAST-STREAM-STREAMS", "ACL2", "COMMON-LISP"), 1831("ALPHA-CHAR-P", "ACL2", "COMMON-LISP"), 1832("BIT", "ACL2", "COMMON-LISP"), 1833("BUILT-IN-CLASS", "ACL2", "COMMON-LISP"), 1834("ALPHANUMERICP", "ACL2", "COMMON-LISP"), 1835("BIT-AND", "ACL2", "COMMON-LISP"), 1836("BUTLAST", "ACL2", "COMMON-LISP"), 1837("AND", "ACL2", "COMMON-LISP"), 1838("BIT-ANDC1", "ACL2", "COMMON-LISP"), 1839("BYTE", "ACL2", "COMMON-LISP"), 1840("APPEND", "ACL2", "COMMON-LISP"), 1841("BIT-ANDC2", "ACL2", "COMMON-LISP"), 1842("BYTE-POSITION", "ACL2", "COMMON-LISP"), 1843("APPLY", "ACL2", "COMMON-LISP"), 1844("BIT-EQV", "ACL2", "COMMON-LISP"), 1845("BYTE-SIZE", "ACL2", "COMMON-LISP"), 1846("APROPOS", "ACL2", "COMMON-LISP"), 1847("BIT-IOR", "ACL2", "COMMON-LISP"), 1848("CAAAAR", "ACL2", "COMMON-LISP"), 1849("APROPOS-LIST", "ACL2", "COMMON-LISP"), 1850("BIT-NAND", "ACL2", "COMMON-LISP"), 1851("CAAADR", "ACL2", "COMMON-LISP"), 1852("AREF", "ACL2", "COMMON-LISP"), 1853("BIT-NOR", "ACL2", "COMMON-LISP"), 1854("CAAAR", "ACL2", "COMMON-LISP"), 1855("ARITHMETIC-ERROR", "ACL2", "COMMON-LISP"), 1856("BIT-NOT", "ACL2", "COMMON-LISP"), 1857("CAADAR", "ACL2", "COMMON-LISP"), 1858("ARITHMETIC-ERROR-OPERANDS", "ACL2", "COMMON-LISP"), 1859("BIT-ORC1", "ACL2", "COMMON-LISP"), 1860("CAADDR", "ACL2", "COMMON-LISP"), 1861("ARITHMETIC-ERROR-OPERATION", "ACL2", "COMMON-LISP"), 1862("BIT-ORC2", "ACL2", "COMMON-LISP"), 1863("CAADR", "ACL2", "COMMON-LISP"), 1864("ARRAY", "ACL2", "COMMON-LISP"), 1865("BIT-VECTOR", "ACL2", "COMMON-LISP"), 1866("CAAR", "ACL2", "COMMON-LISP"), 1867("ARRAY-DIMENSION", "ACL2", "COMMON-LISP"), 1868("BIT-VECTOR-P", "ACL2", "COMMON-LISP"), 1869("CADAAR", "ACL2", "COMMON-LISP"), 1870("ARRAY-DIMENSION-LIMIT", "ACL2", "COMMON-LISP"), 1871("BIT-XOR", "ACL2", "COMMON-LISP"), 1872("CADADR", "ACL2", "COMMON-LISP"), 1873("ARRAY-DIMENSIONS", "ACL2", "COMMON-LISP"), 1874("BLOCK", "ACL2", "COMMON-LISP"), 1875("CADAR", "ACL2", "COMMON-LISP"), 1876("ARRAY-DISPLACEMENT", "ACL2", "COMMON-LISP"), 1877("BOOLE", "ACL2", "COMMON-LISP"), 1878("CADDAR", "ACL2", "COMMON-LISP"), 1879("ARRAY-ELEMENT-TYPE", "ACL2", "COMMON-LISP"), 1880("BOOLE-1", "ACL2", "COMMON-LISP"), 1881("CADDDR", "ACL2", "COMMON-LISP"), 1882("ARRAY-HAS-FILL-POINTER-P", "ACL2", "COMMON-LISP"), 1883("BOOLE-2", "ACL2", "COMMON-LISP"), 1884("CADDR", "ACL2", "COMMON-LISP"), 1885("ARRAY-IN-BOUNDS-P", "ACL2", "COMMON-LISP"), 1886("BOOLE-AND", "ACL2", "COMMON-LISP"), 1887("CADR", "ACL2", "COMMON-LISP"), 1888("ARRAY-RANK", "ACL2", "COMMON-LISP"), 1889("BOOLE-ANDC1", "ACL2", "COMMON-LISP"), 1890("CALL-ARGUMENTS-LIMIT", "ACL2", "COMMON-LISP"), 1891("ARRAY-RANK-LIMIT", "ACL2", "COMMON-LISP"), 1892("BOOLE-ANDC2", "ACL2", "COMMON-LISP"), 1893("CALL-METHOD", "ACL2", "COMMON-LISP"), 1894("ARRAY-ROW-MAJOR-INDEX", "ACL2", "COMMON-LISP"), 1895("BOOLE-C1", "ACL2", "COMMON-LISP"), 1896("CALL-NEXT-METHOD", "ACL2", "COMMON-LISP"), 1897("ARRAY-TOTAL-SIZE", "ACL2", "COMMON-LISP"), 1898("BOOLE-C2", "ACL2", "COMMON-LISP"), 1899("CAR", "ACL2", "COMMON-LISP"), 1900("ARRAY-TOTAL-SIZE-LIMIT", "ACL2", "COMMON-LISP"), 1901("BOOLE-CLR", "ACL2", "COMMON-LISP"), 1902("CASE", "ACL2", "COMMON-LISP"), 1903("ARRAYP", "ACL2", "COMMON-LISP"), 1904("BOOLE-EQV", "ACL2", "COMMON-LISP"), 1905("CATCH", "ACL2", "COMMON-LISP"), 1906("ASH", "ACL2", "COMMON-LISP"), 1907("BOOLE-IOR", "ACL2", "COMMON-LISP"), 1908("CCASE", "ACL2", "COMMON-LISP"), 1909("ASIN", "ACL2", "COMMON-LISP"), 1910("BOOLE-NAND", "ACL2", "COMMON-LISP"), 1911("CDAAAR", "ACL2", "COMMON-LISP"), 1912("ASINH", "ACL2", "COMMON-LISP"), 1913("BOOLE-NOR", "ACL2", "COMMON-LISP"), 1914("CDAADR", "ACL2", "COMMON-LISP"), 1915("ASSERT", "ACL2", "COMMON-LISP"), 1916("BOOLE-ORC1", "ACL2", "COMMON-LISP"), 1917("CDAAR", "ACL2", "COMMON-LISP"), 1918("ASSOC", "ACL2", "COMMON-LISP"), 1919("BOOLE-ORC2", "ACL2", "COMMON-LISP"), 1920("CDADAR", "ACL2", "COMMON-LISP"), 1921("ASSOC-IF", "ACL2", "COMMON-LISP"), 1922("BOOLE-SET", "ACL2", "COMMON-LISP"), 1923("CDADDR", "ACL2", "COMMON-LISP"), 1924("ASSOC-IF-NOT", "ACL2", "COMMON-LISP"), 1925("BOOLE-XOR", "ACL2", "COMMON-LISP"), 1926("CDADR", "ACL2", "COMMON-LISP"), 1927("ATAN", "ACL2", "COMMON-LISP"), 1928("BOOLEAN", "ACL2", "COMMON-LISP"), 1929("CDAR", "ACL2", "COMMON-LISP"), 1930("ATANH", "ACL2", "COMMON-LISP"), 1931("BOTH-CASE-P", "ACL2", "COMMON-LISP"), 1932("CDDAAR", "ACL2", "COMMON-LISP"), 1933("CDDADR", "ACL2", "COMMON-LISP"), 1934("CLEAR-INPUT", "ACL2", "COMMON-LISP"), 1935("COPY-TREE", "ACL2", "COMMON-LISP"), 1936("CDDAR", "ACL2", "COMMON-LISP"), 1937("CLEAR-OUTPUT", "ACL2", "COMMON-LISP"), 1938("COS", "ACL2", "COMMON-LISP"), 1939("CDDDAR", "ACL2", "COMMON-LISP"), 1940("CLOSE", "ACL2", "COMMON-LISP"), 1941("COSH", "ACL2", "COMMON-LISP"), 1942("CDDDDR", "ACL2", "COMMON-LISP"), 1943("CLRHASH", "ACL2", "COMMON-LISP"), 1944("COUNT", "ACL2", "COMMON-LISP"), 1945("CDDDR", "ACL2", "COMMON-LISP"), 1946("CODE-CHAR", "ACL2", "COMMON-LISP"), 1947("COUNT-IF", "ACL2", "COMMON-LISP"), 1948("CDDR", "ACL2", "COMMON-LISP"), 1949("COERCE", "ACL2", "COMMON-LISP"), 1950("COUNT-IF-NOT", "ACL2", "COMMON-LISP"), 1951("CDR", "ACL2", "COMMON-LISP"), 1952("COMPILATION-SPEED", "ACL2", "COMMON-LISP"), 1953("CTYPECASE", "ACL2", "COMMON-LISP"), 1954("CEILING", "ACL2", "COMMON-LISP"), 1955("COMPILE", "ACL2", "COMMON-LISP"), 1956("DEBUG", "ACL2", "COMMON-LISP"), 1957("CELL-ERROR", "ACL2", "COMMON-LISP"), 1958("COMPILE-FILE", "ACL2", "COMMON-LISP"), 1959("DECF", "ACL2", "COMMON-LISP"), 1960("CELL-ERROR-NAME", "ACL2", "COMMON-LISP"), 1961("COMPILE-FILE-PATHNAME", "ACL2", "COMMON-LISP"), 1962("DECLAIM", "ACL2", "COMMON-LISP"), 1963("CERROR", "ACL2", "COMMON-LISP"), 1964("COMPILED-FUNCTION", "ACL2", "COMMON-LISP"), 1965("DECLARATION", "ACL2", "COMMON-LISP"), 1966("CHANGE-CLASS", "ACL2", "COMMON-LISP"), 1967("COMPILED-FUNCTION-P", "ACL2", "COMMON-LISP"), 1968("DECLARE", "ACL2", "COMMON-LISP"), 1969("CHAR", "ACL2", "COMMON-LISP"), 1970("COMPILER-MACRO", "ACL2", "COMMON-LISP"), 1971("DECODE-FLOAT", "ACL2", "COMMON-LISP"), 1972("CHAR-CODE", "ACL2", "COMMON-LISP"), 1973("COMPILER-MACRO-FUNCTION", "ACL2", "COMMON-LISP"), 1974("DECODE-UNIVERSAL-TIME", "ACL2", "COMMON-LISP"), 1975("CHAR-CODE-LIMIT", "ACL2", "COMMON-LISP"), 1976("COMPLEMENT", "ACL2", "COMMON-LISP"), 1977("DEFCLASS", "ACL2", "COMMON-LISP"), 1978("CHAR-DOWNCASE", "ACL2", "COMMON-LISP"), 1979("COMPLEX", "ACL2", "COMMON-LISP"), 1980("DEFCONSTANT", "ACL2", "COMMON-LISP"), 1981("CHAR-EQUAL", "ACL2", "COMMON-LISP"), 1982("COMPLEXP", "ACL2", "COMMON-LISP"), 1983("DEFGENERIC", "ACL2", "COMMON-LISP"), 1984("CHAR-GREATERP", "ACL2", "COMMON-LISP"), 1985("COMPUTE-APPLICABLE-METHODS", "ACL2", "COMMON-LISP"), 1986("DEFINE-COMPILER-MACRO", "ACL2", "COMMON-LISP"), 1987("CHAR-INT", "ACL2", "COMMON-LISP"), 1988("COMPUTE-RESTARTS", "ACL2", "COMMON-LISP"), 1989("DEFINE-CONDITION", "ACL2", "COMMON-LISP"), 1990("CHAR-LESSP", "ACL2", "COMMON-LISP"), 1991("CONCATENATE", "ACL2", "COMMON-LISP"), 1992("DEFINE-METHOD-COMBINATION", "ACL2", "COMMON-LISP"), 1993("CHAR-NAME", "ACL2", "COMMON-LISP"), 1994("CONCATENATED-STREAM", "ACL2", "COMMON-LISP"), 1995("DEFINE-MODIFY-MACRO", "ACL2", "COMMON-LISP"), 1996("CHAR-NOT-EQUAL", "ACL2", "COMMON-LISP"), 1997("CONCATENATED-STREAM-STREAMS", "ACL2", "COMMON-LISP"), 1998("DEFINE-SETF-EXPANDER", "ACL2", "COMMON-LISP"), 1999("CHAR-NOT-GREATERP", "ACL2", "COMMON-LISP"), 2000("COND", "ACL2", "COMMON-LISP"), 2001("DEFINE-SYMBOL-MACRO", "ACL2", "COMMON-LISP"), 2002("CHAR-NOT-LESSP", "ACL2", "COMMON-LISP"), 2003("CONDITION", "ACL2", "COMMON-LISP"), 2004("DEFMACRO", "ACL2", "COMMON-LISP"), 2005("CHAR-UPCASE", "ACL2", "COMMON-LISP"), 2006("CONJUGATE", "ACL2", "COMMON-LISP"), 2007("DEFMETHOD", "ACL2", "COMMON-LISP"), 2008("CHAR/=", "ACL2", "COMMON-LISP"), 2009("CONS", "ACL2", "COMMON-LISP"), 2010("DEFPACKAGE", "ACL2", "COMMON-LISP"), 2011("CHAR<", "ACL2", "COMMON-LISP"), 2012("CONSP", "ACL2", "COMMON-LISP"), 2013("DEFPARAMETER", "ACL2", "COMMON-LISP"), 2014("CHAR<=", "ACL2", "COMMON-LISP"), 2015("CONSTANTLY", "ACL2", "COMMON-LISP"), 2016("DEFSETF", "ACL2", "COMMON-LISP"), 2017("CHAR=", "ACL2", "COMMON-LISP"), 2018("CONSTANTP", "ACL2", "COMMON-LISP"), 2019("DEFSTRUCT", "ACL2", "COMMON-LISP"), 2020("CHAR>", "ACL2", "COMMON-LISP"), 2021("CONTINUE", "ACL2", "COMMON-LISP"), 2022("DEFTYPE", "ACL2", "COMMON-LISP"), 2023("CHAR>=", "ACL2", "COMMON-LISP"), 2024("CONTROL-ERROR", "ACL2", "COMMON-LISP"), 2025("DEFUN", "ACL2", "COMMON-LISP"), 2026("CHARACTER", "ACL2", "COMMON-LISP"), 2027("COPY-ALIST", "ACL2", "COMMON-LISP"), 2028("DEFVAR", "ACL2", "COMMON-LISP"), 2029("CHARACTERP", "ACL2", "COMMON-LISP"), 2030("COPY-LIST", "ACL2", "COMMON-LISP"), 2031("DELETE", "ACL2", "COMMON-LISP"), 2032("CHECK-TYPE", "ACL2", "COMMON-LISP"), 2033("COPY-PPRINT-DISPATCH", "ACL2", "COMMON-LISP"), 2034("DELETE-DUPLICATES", "ACL2", "COMMON-LISP"), 2035("CIS", "ACL2", "COMMON-LISP"), 2036("COPY-READTABLE", "ACL2", "COMMON-LISP"), 2037("DELETE-FILE", "ACL2", "COMMON-LISP"), 2038("CLASS", "ACL2", "COMMON-LISP"), 2039("COPY-SEQ", "ACL2", "COMMON-LISP"), 2040("DELETE-IF", "ACL2", "COMMON-LISP"), 2041("CLASS-NAME", "ACL2", "COMMON-LISP"), 2042("COPY-STRUCTURE", "ACL2", "COMMON-LISP"), 2043("DELETE-IF-NOT", "ACL2", "COMMON-LISP"), 2044("CLASS-OF", "ACL2", "COMMON-LISP"), 2045("COPY-SYMBOL", "ACL2", "COMMON-LISP"), 2046("DELETE-PACKAGE", "ACL2", "COMMON-LISP"), 2047("DENOMINATOR", "ACL2", "COMMON-LISP"), 2048("EQ", "ACL2", "COMMON-LISP"), 2049("DEPOSIT-FIELD", "ACL2", "COMMON-LISP"), 2050("EQL", "ACL2", "COMMON-LISP"), 2051("DESCRIBE", "ACL2", "COMMON-LISP"), 2052("EQUAL", "ACL2", "COMMON-LISP"), 2053("DESCRIBE-OBJECT", "ACL2", "COMMON-LISP"), 2054("EQUALP", "ACL2", "COMMON-LISP"), 2055("DESTRUCTURING-BIND", "ACL2", "COMMON-LISP"), 2056("ERROR", "ACL2", "COMMON-LISP"), 2057("DIGIT-CHAR", "ACL2", "COMMON-LISP"), 2058("ETYPECASE", "ACL2", "COMMON-LISP"), 2059("DIGIT-CHAR-P", "ACL2", "COMMON-LISP"), 2060("EVAL", "ACL2", "COMMON-LISP"), 2061("DIRECTORY", "ACL2", "COMMON-LISP"), 2062("EVAL-WHEN", "ACL2", "COMMON-LISP"), 2063("DIRECTORY-NAMESTRING", "ACL2", "COMMON-LISP"), 2064("EVENP", "ACL2", "COMMON-LISP"), 2065("DISASSEMBLE", "ACL2", "COMMON-LISP"), 2066("EVERY", "ACL2", "COMMON-LISP"), 2067("DIVISION-BY-ZERO", "ACL2", "COMMON-LISP"), 2068("EXP", "ACL2", "COMMON-LISP"), 2069("DO", "ACL2", "COMMON-LISP"), 2070("EXPORT", "ACL2", "COMMON-LISP"), 2071("DO*", "ACL2", "COMMON-LISP"), 2072("EXPT", "ACL2", "COMMON-LISP"), 2073("DO-ALL-SYMBOLS", "ACL2", "COMMON-LISP"), 2074("EXTENDED-CHAR", "ACL2", "COMMON-LISP"), 2075("DO-EXTERNAL-SYMBOLS", "ACL2", "COMMON-LISP"), 2076("FBOUNDP", "ACL2", "COMMON-LISP"), 2077("DO-SYMBOLS", "ACL2", "COMMON-LISP"), 2078("FCEILING", "ACL2", "COMMON-LISP"), 2079("DOCUMENTATION", "ACL2", "COMMON-LISP"), 2080("FDEFINITION", "ACL2", "COMMON-LISP"), 2081("DOLIST", "ACL2", "COMMON-LISP"), 2082("FFLOOR", "ACL2", "COMMON-LISP"), 2083("DOTIMES", "ACL2", "COMMON-LISP"), 2084("FIFTH", "ACL2", "COMMON-LISP"), 2085("DOUBLE-FLOAT", "ACL2", "COMMON-LISP"), 2086("FILE-AUTHOR", "ACL2", "COMMON-LISP"), 2087("DOUBLE-FLOAT-EPSILON", "ACL2", "COMMON-LISP"), 2088("FILE-ERROR", "ACL2", "COMMON-LISP"), 2089("DOUBLE-FLOAT-NEGATIVE-EPSILON", "ACL2", "COMMON-LISP"), 2090("FILE-ERROR-PATHNAME", "ACL2", "COMMON-LISP"), 2091("DPB", "ACL2", "COMMON-LISP"), 2092("FILE-LENGTH", "ACL2", "COMMON-LISP"), 2093("DRIBBLE", "ACL2", "COMMON-LISP"), 2094("FILE-NAMESTRING", "ACL2", "COMMON-LISP"), 2095("DYNAMIC-EXTENT", "ACL2", "COMMON-LISP"), 2096("FILE-POSITION", "ACL2", "COMMON-LISP"), 2097("ECASE", "ACL2", "COMMON-LISP"), 2098("FILE-STREAM", "ACL2", "COMMON-LISP"), 2099("ECHO-STREAM", "ACL2", "COMMON-LISP"), 2100("FILE-STRING-LENGTH", "ACL2", "COMMON-LISP"), 2101("ECHO-STREAM-INPUT-STREAM", "ACL2", "COMMON-LISP"), 2102("FILE-WRITE-DATE", "ACL2", "COMMON-LISP"), 2103("ECHO-STREAM-OUTPUT-STREAM", "ACL2", "COMMON-LISP"), 2104("FILL", "ACL2", "COMMON-LISP"), 2105("ED", "ACL2", "COMMON-LISP"), 2106("FILL-POINTER", "ACL2", "COMMON-LISP"), 2107("EIGHTH", "ACL2", "COMMON-LISP"), 2108("FIND", "ACL2", "COMMON-LISP"), 2109("ELT", "ACL2", "COMMON-LISP"), 2110("FIND-ALL-SYMBOLS", "ACL2", "COMMON-LISP"), 2111("ENCODE-UNIVERSAL-TIME", "ACL2", "COMMON-LISP"), 2112("FIND-CLASS", "ACL2", "COMMON-LISP"), 2113("END-OF-FILE", "ACL2", "COMMON-LISP"), 2114("FIND-IF", "ACL2", "COMMON-LISP"), 2115("ENDP", "ACL2", "COMMON-LISP"), 2116("FIND-IF-NOT", "ACL2", "COMMON-LISP"), 2117("ENOUGH-NAMESTRING", "ACL2", "COMMON-LISP"), 2118("FIND-METHOD", "ACL2", "COMMON-LISP"), 2119("ENSURE-DIRECTORIES-EXIST", "ACL2", "COMMON-LISP"), 2120("FIND-PACKAGE", "ACL2", "COMMON-LISP"), 2121("ENSURE-GENERIC-FUNCTION", "ACL2", "COMMON-LISP"), 2122("FIND-RESTART", "ACL2", "COMMON-LISP"), 2123("FIND-SYMBOL", "ACL2", "COMMON-LISP"), 2124("GET-INTERNAL-RUN-TIME", "ACL2", "COMMON-LISP"), 2125("FINISH-OUTPUT", "ACL2", "COMMON-LISP"), 2126("GET-MACRO-CHARACTER", "ACL2", "COMMON-LISP"), 2127("FIRST", "ACL2", "COMMON-LISP"), 2128("GET-OUTPUT-STREAM-STRING", "ACL2", "COMMON-LISP"), 2129("FIXNUM", "ACL2", "COMMON-LISP"), 2130("GET-PROPERTIES", "ACL2", "COMMON-LISP"), 2131("FLET", "ACL2", "COMMON-LISP"), 2132("GET-SETF-EXPANSION", "ACL2", "COMMON-LISP"), 2133("FLOAT", "ACL2", "COMMON-LISP"), 2134("GET-UNIVERSAL-TIME", "ACL2", "COMMON-LISP"), 2135("FLOAT-DIGITS", "ACL2", "COMMON-LISP"), 2136("GETF", "ACL2", "COMMON-LISP"), 2137("FLOAT-PRECISION", "ACL2", "COMMON-LISP"), 2138("GETHASH", "ACL2", "COMMON-LISP"), 2139("FLOAT-RADIX", "ACL2", "COMMON-LISP"), 2140("GO", "ACL2", "COMMON-LISP"), 2141("FLOAT-SIGN", "ACL2", "COMMON-LISP"), 2142("GRAPHIC-CHAR-P", "ACL2", "COMMON-LISP"), 2143("FLOATING-POINT-INEXACT", "ACL2", "COMMON-LISP"), 2144("HANDLER-BIND", "ACL2", "COMMON-LISP"), 2145("FLOATING-POINT-INVALID-OPERATION", "ACL2", "COMMON-LISP"), 2146("HANDLER-CASE", "ACL2", "COMMON-LISP"), 2147("FLOATING-POINT-OVERFLOW", "ACL2", "COMMON-LISP"), 2148("HASH-TABLE", "ACL2", "COMMON-LISP"), 2149("FLOATING-POINT-UNDERFLOW", "ACL2", "COMMON-LISP"), 2150("HASH-TABLE-COUNT", "ACL2", "COMMON-LISP"), 2151("FLOATP", "ACL2", "COMMON-LISP"), 2152("HASH-TABLE-P", "ACL2", "COMMON-LISP"), 2153("FLOOR", "ACL2", "COMMON-LISP"), 2154("HASH-TABLE-REHASH-SIZE", "ACL2", "COMMON-LISP"), 2155("FMAKUNBOUND", "ACL2", "COMMON-LISP"), 2156("HASH-TABLE-REHASH-THRESHOLD", "ACL2", "COMMON-LISP"), 2157("FORCE-OUTPUT", "ACL2", "COMMON-LISP"), 2158("HASH-TABLE-SIZE", "ACL2", "COMMON-LISP"), 2159("FORMAT", "ACL2", "COMMON-LISP"), 2160("HASH-TABLE-TEST", "ACL2", "COMMON-LISP"), 2161("FORMATTER", "ACL2", "COMMON-LISP"), 2162("HOST-NAMESTRING", "ACL2", "COMMON-LISP"), 2163("FOURTH", "ACL2", "COMMON-LISP"), 2164("IDENTITY", "ACL2", "COMMON-LISP"), 2165("FRESH-LINE", "ACL2", "COMMON-LISP"), 2166("IF", "ACL2", "COMMON-LISP"), 2167("FROUND", "ACL2", "COMMON-LISP"), 2168("IGNORABLE", "ACL2", "COMMON-LISP"), 2169("FTRUNCATE", "ACL2", "COMMON-LISP"), 2170("IGNORE", "ACL2", "COMMON-LISP"), 2171("FTYPE", "ACL2", "COMMON-LISP"), 2172("IGNORE-ERRORS", "ACL2", "COMMON-LISP"), 2173("FUNCALL", "ACL2", "COMMON-LISP"), 2174("IMAGPART", "ACL2", "COMMON-LISP"), 2175("FUNCTION", "ACL2", "COMMON-LISP"), 2176("IMPORT", "ACL2", "COMMON-LISP"), 2177("FUNCTION-KEYWORDS", "ACL2", "COMMON-LISP"), 2178("IN-PACKAGE", "ACL2", "COMMON-LISP"), 2179("FUNCTION-LAMBDA-EXPRESSION", "ACL2", "COMMON-LISP"), 2180("INCF", "ACL2", "COMMON-LISP"), 2181("FUNCTIONP", "ACL2", "COMMON-LISP"), 2182("INITIALIZE-INSTANCE", "ACL2", "COMMON-LISP"), 2183("GCD", "ACL2", "COMMON-LISP"), 2184("INLINE", "ACL2", "COMMON-LISP"), 2185("GENERIC-FUNCTION", "ACL2", "COMMON-LISP"), 2186("INPUT-STREAM-P", "ACL2", "COMMON-LISP"), 2187("GENSYM", "ACL2", "COMMON-LISP"), 2188("INSPECT", "ACL2", "COMMON-LISP"), 2189("GENTEMP", "ACL2", "COMMON-LISP"), 2190("INTEGER", "ACL2", "COMMON-LISP"), 2191("GET", "ACL2", "COMMON-LISP"), 2192("INTEGER-DECODE-FLOAT", "ACL2", "COMMON-LISP"), 2193("GET-DECODED-TIME", "ACL2", "COMMON-LISP"), 2194("INTEGER-LENGTH", "ACL2", "COMMON-LISP"), 2195("GET-DISPATCH-MACRO-CHARACTER", "ACL2", "COMMON-LISP"), 2196("INTEGERP", "ACL2", "COMMON-LISP"), 2197("GET-INTERNAL-REAL-TIME", "ACL2", "COMMON-LISP"), 2198("INTERACTIVE-STREAM-P", "ACL2", "COMMON-LISP"), 2199("INTERN", "ACL2", "COMMON-LISP"), 2200("LISP-IMPLEMENTATION-TYPE", "ACL2", "COMMON-LISP"), 2201("INTERNAL-TIME-UNITS-PER-SECOND", "ACL2", "COMMON-LISP"), 2202("LISP-IMPLEMENTATION-VERSION", "ACL2", "COMMON-LISP"), 2203("INTERSECTION", "ACL2", "COMMON-LISP"), 2204("LIST", "ACL2", "COMMON-LISP"), 2205("INVALID-METHOD-ERROR", "ACL2", "COMMON-LISP"), 2206("LIST*", "ACL2", "COMMON-LISP"), 2207("INVOKE-DEBUGGER", "ACL2", "COMMON-LISP"), 2208("LIST-ALL-PACKAGES", "ACL2", "COMMON-LISP"), 2209("INVOKE-RESTART", "ACL2", "COMMON-LISP"), 2210("LIST-LENGTH", "ACL2", "COMMON-LISP"), 2211("INVOKE-RESTART-INTERACTIVELY", "ACL2", "COMMON-LISP"), 2212("LISTEN", "ACL2", "COMMON-LISP"), 2213("ISQRT", "ACL2", "COMMON-LISP"), 2214("LISTP", "ACL2", "COMMON-LISP"), 2215("KEYWORD", "ACL2", "COMMON-LISP"), 2216("LOAD", "ACL2", "COMMON-LISP"), 2217("KEYWORDP", "ACL2", "COMMON-LISP"), 2218("LOAD-LOGICAL-PATHNAME-TRANSLATIONS", "ACL2", "COMMON-LISP"), 2219("LABELS", "ACL2", "COMMON-LISP"), 2220("LOAD-TIME-VALUE", "ACL2", "COMMON-LISP"), 2221("LAMBDA", "ACL2", "COMMON-LISP"), 2222("LOCALLY", "ACL2", "COMMON-LISP"), 2223("LAMBDA-LIST-KEYWORDS", "ACL2", "COMMON-LISP"), 2224("LOG", "ACL2", "COMMON-LISP"), 2225("LAMBDA-PARAMETERS-LIMIT", "ACL2", "COMMON-LISP"), 2226("LOGAND", "ACL2", "COMMON-LISP"), 2227("LAST", "ACL2", "COMMON-LISP"), 2228("LOGANDC1", "ACL2", "COMMON-LISP"), 2229("LCM", "ACL2", "COMMON-LISP"), 2230("LOGANDC2", "ACL2", "COMMON-LISP"), 2231("LDB", "ACL2", "COMMON-LISP"), 2232("LOGBITP", "ACL2", "COMMON-LISP"), 2233("LDB-TEST", "ACL2", "COMMON-LISP"), 2234("LOGCOUNT", "ACL2", "COMMON-LISP"), 2235("LDIFF", "ACL2", "COMMON-LISP"), 2236("LOGEQV", "ACL2", "COMMON-LISP"), 2237("LEAST-NEGATIVE-DOUBLE-FLOAT", "ACL2", "COMMON-LISP"), 2238("LOGICAL-PATHNAME", "ACL2", "COMMON-LISP"), 2239("LEAST-NEGATIVE-LONG-FLOAT", "ACL2", "COMMON-LISP"), 2240("LOGICAL-PATHNAME-TRANSLATIONS", "ACL2", "COMMON-LISP"), 2241("LEAST-NEGATIVE-NORMALIZED-DOUBLE-FLOAT", "ACL2", "COMMON-LISP"), 2242("LOGIOR", "ACL2", "COMMON-LISP"), 2243("LEAST-NEGATIVE-NORMALIZED-LONG-FLOAT", "ACL2", "COMMON-LISP"), 2244("LOGNAND", "ACL2", "COMMON-LISP"), 2245("LEAST-NEGATIVE-NORMALIZED-SHORT-FLOAT", "ACL2", "COMMON-LISP"), 2246("LOGNOR", "ACL2", "COMMON-LISP"), 2247("LEAST-NEGATIVE-NORMALIZED-SINGLE-FLOAT", "ACL2", "COMMON-LISP"), 2248("LOGNOT", "ACL2", "COMMON-LISP"), 2249("LEAST-NEGATIVE-SHORT-FLOAT", "ACL2", "COMMON-LISP"), 2250("LOGORC1", "ACL2", "COMMON-LISP"), 2251("LEAST-NEGATIVE-SINGLE-FLOAT", "ACL2", "COMMON-LISP"), 2252("LOGORC2", "ACL2", "COMMON-LISP"), 2253("LEAST-POSITIVE-DOUBLE-FLOAT", "ACL2", "COMMON-LISP"), 2254("LOGTEST", "ACL2", "COMMON-LISP"), 2255("LEAST-POSITIVE-LONG-FLOAT", "ACL2", "COMMON-LISP"), 2256("LOGXOR", "ACL2", "COMMON-LISP"), 2257("LEAST-POSITIVE-NORMALIZED-DOUBLE-FLOAT", "ACL2", "COMMON-LISP"), 2258("LONG-FLOAT", "ACL2", "COMMON-LISP"), 2259("LEAST-POSITIVE-NORMALIZED-LONG-FLOAT", "ACL2", "COMMON-LISP"), 2260("LONG-FLOAT-EPSILON", "ACL2", "COMMON-LISP"), 2261("LEAST-POSITIVE-NORMALIZED-SHORT-FLOAT", "ACL2", "COMMON-LISP"), 2262("LONG-FLOAT-NEGATIVE-EPSILON", "ACL2", "COMMON-LISP"), 2263("LEAST-POSITIVE-NORMALIZED-SINGLE-FLOAT", "ACL2", "COMMON-LISP"), 2264("LONG-SITE-NAME", "ACL2", "COMMON-LISP"), 2265("LEAST-POSITIVE-SHORT-FLOAT", "ACL2", "COMMON-LISP"), 2266("LOOP", "ACL2", "COMMON-LISP"), 2267("LEAST-POSITIVE-SINGLE-FLOAT", "ACL2", "COMMON-LISP"), 2268("LOOP-FINISH", "ACL2", "COMMON-LISP"), 2269("LENGTH", "ACL2", "COMMON-LISP"), 2270("LOWER-CASE-P", "ACL2", "COMMON-LISP"), 2271("LET", "ACL2", "COMMON-LISP"), 2272("MACHINE-INSTANCE", "ACL2", "COMMON-LISP"), 2273("LET*", "ACL2", "COMMON-LISP"), 2274("MACHINE-TYPE", "ACL2", "COMMON-LISP"), 2275("MACHINE-VERSION", "ACL2", "COMMON-LISP"), 2276("MASK-FIELD", "ACL2", "COMMON-LISP"), 2277("MACRO-FUNCTION", "ACL2", "COMMON-LISP"), 2278("MAX", "ACL2", "COMMON-LISP"), 2279("MACROEXPAND", "ACL2", "COMMON-LISP"), 2280("MEMBER", "ACL2", "COMMON-LISP"), 2281("MACROEXPAND-1", "ACL2", "COMMON-LISP"), 2282("MEMBER-IF", "ACL2", "COMMON-LISP"), 2283("MACROLET", "ACL2", "COMMON-LISP"), 2284("MEMBER-IF-NOT", "ACL2", "COMMON-LISP"), 2285("MAKE-ARRAY", "ACL2", "COMMON-LISP"), 2286("MERGE", "ACL2", "COMMON-LISP"), 2287("MAKE-BROADCAST-STREAM", "ACL2", "COMMON-LISP"), 2288("MERGE-PATHNAMES", "ACL2", "COMMON-LISP"), 2289("MAKE-CONCATENATED-STREAM", "ACL2", "COMMON-LISP"), 2290("METHOD", "ACL2", "COMMON-LISP"), 2291("MAKE-CONDITION", "ACL2", "COMMON-LISP"), 2292("METHOD-COMBINATION", "ACL2", "COMMON-LISP"), 2293("MAKE-DISPATCH-MACRO-CHARACTER", "ACL2", "COMMON-LISP"), 2294("METHOD-COMBINATION-ERROR", "ACL2", "COMMON-LISP"), 2295("MAKE-ECHO-STREAM", "ACL2", "COMMON-LISP"), 2296("METHOD-QUALIFIERS", "ACL2", "COMMON-LISP"), 2297("MAKE-HASH-TABLE", "ACL2", "COMMON-LISP"), 2298("MIN", "ACL2", "COMMON-LISP"), 2299("MAKE-INSTANCE", "ACL2", "COMMON-LISP"), 2300("MINUSP", "ACL2", "COMMON-LISP"), 2301("MAKE-INSTANCES-OBSOLETE", "ACL2", "COMMON-LISP"), 2302("MISMATCH", "ACL2", "COMMON-LISP"), 2303("MAKE-LIST", "ACL2", "COMMON-LISP"), 2304("MOD", "ACL2", "COMMON-LISP"), 2305("MAKE-LOAD-FORM", "ACL2", "COMMON-LISP"), 2306("MOST-NEGATIVE-DOUBLE-FLOAT", "ACL2", "COMMON-LISP"), 2307("MAKE-LOAD-FORM-SAVING-SLOTS", "ACL2", "COMMON-LISP"), 2308("MOST-NEGATIVE-FIXNUM", "ACL2", "COMMON-LISP"), 2309("MAKE-METHOD", "ACL2", "COMMON-LISP"), 2310("MOST-NEGATIVE-LONG-FLOAT", "ACL2", "COMMON-LISP"), 2311("MAKE-PACKAGE", "ACL2", "COMMON-LISP"), 2312("MOST-NEGATIVE-SHORT-FLOAT", "ACL2", "COMMON-LISP"), 2313("MAKE-PATHNAME", "ACL2", "COMMON-LISP"), 2314("MOST-NEGATIVE-SINGLE-FLOAT", "ACL2", "COMMON-LISP"), 2315("MAKE-RANDOM-STATE", "ACL2", "COMMON-LISP"), 2316("MOST-POSITIVE-DOUBLE-FLOAT", "ACL2", "COMMON-LISP"), 2317("MAKE-SEQUENCE", "ACL2", "COMMON-LISP"), 2318("MOST-POSITIVE-FIXNUM", "ACL2", "COMMON-LISP"), 2319("MAKE-STRING", "ACL2", "COMMON-LISP"), 2320("MOST-POSITIVE-LONG-FLOAT", "ACL2", "COMMON-LISP"), 2321("MAKE-STRING-INPUT-STREAM", "ACL2", "COMMON-LISP"), 2322("MOST-POSITIVE-SHORT-FLOAT", "ACL2", "COMMON-LISP"), 2323("MAKE-STRING-OUTPUT-STREAM", "ACL2", "COMMON-LISP"), 2324("MOST-POSITIVE-SINGLE-FLOAT", "ACL2", "COMMON-LISP"), 2325("MAKE-SYMBOL", "ACL2", "COMMON-LISP"), 2326("MUFFLE-WARNING", "ACL2", "COMMON-LISP"), 2327("MAKE-SYNONYM-STREAM", "ACL2", "COMMON-LISP"), 2328("MULTIPLE-VALUE-BIND", "ACL2", "COMMON-LISP"), 2329("MAKE-TWO-WAY-STREAM", "ACL2", "COMMON-LISP"), 2330("MULTIPLE-VALUE-CALL", "ACL2", "COMMON-LISP"), 2331("MAKUNBOUND", "ACL2", "COMMON-LISP"), 2332("MULTIPLE-VALUE-LIST", "ACL2", "COMMON-LISP"), 2333("MAP", "ACL2", "COMMON-LISP"), 2334("MULTIPLE-VALUE-PROG1", "ACL2", "COMMON-LISP"), 2335("MAP-INTO", "ACL2", "COMMON-LISP"), 2336("MULTIPLE-VALUE-SETQ", "ACL2", "COMMON-LISP"), 2337("MAPC", "ACL2", "COMMON-LISP"), 2338("MULTIPLE-VALUES-LIMIT", "ACL2", "COMMON-LISP"), 2339("MAPCAN", "ACL2", "COMMON-LISP"), 2340("NAME-CHAR", "ACL2", "COMMON-LISP"), 2341("MAPCAR", "ACL2", "COMMON-LISP"), 2342("NAMESTRING", "ACL2", "COMMON-LISP"), 2343("MAPCON", "ACL2", "COMMON-LISP"), 2344("NBUTLAST", "ACL2", "COMMON-LISP"), 2345("MAPHASH", "ACL2", "COMMON-LISP"), 2346("NCONC", "ACL2", "COMMON-LISP"), 2347("MAPL", "ACL2", "COMMON-LISP"), 2348("NEXT-METHOD-P", "ACL2", "COMMON-LISP"), 2349("MAPLIST", "ACL2", "COMMON-LISP"), 2350("NIL", "ACL2", "COMMON-LISP"), 2351("NINTERSECTION", "ACL2", "COMMON-LISP"), 2352("PACKAGE-ERROR", "ACL2", "COMMON-LISP"), 2353("NINTH", "ACL2", "COMMON-LISP"), 2354("PACKAGE-ERROR-PACKAGE", "ACL2", "COMMON-LISP"), 2355("NO-APPLICABLE-METHOD", "ACL2", "COMMON-LISP"), 2356("PACKAGE-NAME", "ACL2", "COMMON-LISP"), 2357("NO-NEXT-METHOD", "ACL2", "COMMON-LISP"), 2358("PACKAGE-NICKNAMES", "ACL2", "COMMON-LISP"), 2359("NOT", "ACL2", "COMMON-LISP"), 2360("PACKAGE-SHADOWING-SYMBOLS", "ACL2", "COMMON-LISP"), 2361("NOTANY", "ACL2", "COMMON-LISP"), 2362("PACKAGE-USE-LIST", "ACL2", "COMMON-LISP"), 2363("NOTEVERY", "ACL2", "COMMON-LISP"), 2364("PACKAGE-USED-BY-LIST", "ACL2", "COMMON-LISP"), 2365("NOTINLINE", "ACL2", "COMMON-LISP"), 2366("PACKAGEP", "ACL2", "COMMON-LISP"), 2367("NRECONC", "ACL2", "COMMON-LISP"), 2368("PAIRLIS", "ACL2", "COMMON-LISP"), 2369("NREVERSE", "ACL2", "COMMON-LISP"), 2370("PARSE-ERROR", "ACL2", "COMMON-LISP"), 2371("NSET-DIFFERENCE", "ACL2", "COMMON-LISP"), 2372("PARSE-INTEGER", "ACL2", "COMMON-LISP"), 2373("NSET-EXCLUSIVE-OR", "ACL2", "COMMON-LISP"), 2374("PARSE-NAMESTRING", "ACL2", "COMMON-LISP"), 2375("NSTRING-CAPITALIZE", "ACL2", "COMMON-LISP"), 2376("PATHNAME", "ACL2", "COMMON-LISP"), 2377("NSTRING-DOWNCASE", "ACL2", "COMMON-LISP"), 2378("PATHNAME-DEVICE", "ACL2", "COMMON-LISP"), 2379("NSTRING-UPCASE", "ACL2", "COMMON-LISP"), 2380("PATHNAME-DIRECTORY", "ACL2", "COMMON-LISP"), 2381("NSUBLIS", "ACL2", "COMMON-LISP"), 2382("PATHNAME-HOST", "ACL2", "COMMON-LISP"), 2383("NSUBST", "ACL2", "COMMON-LISP"), 2384("PATHNAME-MATCH-P", "ACL2", "COMMON-LISP"), 2385("NSUBST-IF", "ACL2", "COMMON-LISP"), 2386("PATHNAME-NAME", "ACL2", "COMMON-LISP"), 2387("NSUBST-IF-NOT", "ACL2", "COMMON-LISP"), 2388("PATHNAME-TYPE", "ACL2", "COMMON-LISP"), 2389("NSUBSTITUTE", "ACL2", "COMMON-LISP"), 2390("PATHNAME-VERSION", "ACL2", "COMMON-LISP"), 2391("NSUBSTITUTE-IF", "ACL2", "COMMON-LISP"), 2392("PATHNAMEP", "ACL2", "COMMON-LISP"), 2393("NSUBSTITUTE-IF-NOT", "ACL2", "COMMON-LISP"), 2394("PEEK-CHAR", "ACL2", "COMMON-LISP"), 2395("NTH", "ACL2", "COMMON-LISP"), 2396("PHASE", "ACL2", "COMMON-LISP"), 2397("NTH-VALUE", "ACL2", "COMMON-LISP"), 2398("PI", "ACL2", "COMMON-LISP"), 2399("NTHCDR", "ACL2", "COMMON-LISP"), 2400("PLUSP", "ACL2", "COMMON-LISP"), 2401("NULL", "ACL2", "COMMON-LISP"), 2402("POP", "ACL2", "COMMON-LISP"), 2403("NUMBER", "ACL2", "COMMON-LISP"), 2404("POSITION", "ACL2", "COMMON-LISP"), 2405("NUMBERP", "ACL2", "COMMON-LISP"), 2406("POSITION-IF", "ACL2", "COMMON-LISP"), 2407("NUMERATOR", "ACL2", "COMMON-LISP"), 2408("POSITION-IF-NOT", "ACL2", "COMMON-LISP"), 2409("NUNION", "ACL2", "COMMON-LISP"), 2410("PPRINT", "ACL2", "COMMON-LISP"), 2411("ODDP", "ACL2", "COMMON-LISP"), 2412("PPRINT-DISPATCH", "ACL2", "COMMON-LISP"), 2413("OPEN", "ACL2", "COMMON-LISP"), 2414("PPRINT-EXIT-IF-LIST-EXHAUSTED", "ACL2", "COMMON-LISP"), 2415("OPEN-STREAM-P", "ACL2", "COMMON-LISP"), 2416("PPRINT-FILL", "ACL2", "COMMON-LISP"), 2417("OPTIMIZE", "ACL2", "COMMON-LISP"), 2418("PPRINT-INDENT", "ACL2", "COMMON-LISP"), 2419("OR", "ACL2", "COMMON-LISP"), 2420("PPRINT-LINEAR", "ACL2", "COMMON-LISP"), 2421("OTHERWISE", "ACL2", "COMMON-LISP"), 2422("PPRINT-LOGICAL-BLOCK", "ACL2", "COMMON-LISP"), 2423("OUTPUT-STREAM-P", "ACL2", "COMMON-LISP"), 2424("PPRINT-NEWLINE", "ACL2", "COMMON-LISP"), 2425("PACKAGE", "ACL2", "COMMON-LISP"), 2426("PPRINT-POP", "ACL2", "COMMON-LISP"), 2427("PPRINT-TAB", "ACL2", "COMMON-LISP"), 2428("READ-CHAR", "ACL2", "COMMON-LISP"), 2429("PPRINT-TABULAR", "ACL2", "COMMON-LISP"), 2430("READ-CHAR-NO-HANG", "ACL2", "COMMON-LISP"), 2431("PRIN1", "ACL2", "COMMON-LISP"), 2432("READ-DELIMITED-LIST", "ACL2", "COMMON-LISP"), 2433("PRIN1-TO-STRING", "ACL2", "COMMON-LISP"), 2434("READ-FROM-STRING", "ACL2", "COMMON-LISP"), 2435("PRINC", "ACL2", "COMMON-LISP"), 2436("READ-LINE", "ACL2", "COMMON-LISP"), 2437("PRINC-TO-STRING", "ACL2", "COMMON-LISP"), 2438("READ-PRESERVING-WHITESPACE", "ACL2", "COMMON-LISP"), 2439("PRINT", "ACL2", "COMMON-LISP"), 2440("READ-SEQUENCE", "ACL2", "COMMON-LISP"), 2441("PRINT-NOT-READABLE", "ACL2", "COMMON-LISP"), 2442("READER-ERROR", "ACL2", "COMMON-LISP"), 2443("PRINT-NOT-READABLE-OBJECT", "ACL2", "COMMON-LISP"), 2444("READTABLE", "ACL2", "COMMON-LISP"), 2445("PRINT-OBJECT", "ACL2", "COMMON-LISP"), 2446("READTABLE-CASE", "ACL2", "COMMON-LISP"), 2447("PRINT-UNREADABLE-OBJECT", "ACL2", "COMMON-LISP"), 2448("READTABLEP", "ACL2", "COMMON-LISP"), 2449("PROBE-FILE", "ACL2", "COMMON-LISP"), 2450("REAL", "ACL2", "COMMON-LISP"), 2451("PROCLAIM", "ACL2", "COMMON-LISP"), 2452("REALP", "ACL2", "COMMON-LISP"), 2453("PROG", "ACL2", "COMMON-LISP"), 2454("REALPART", "ACL2", "COMMON-LISP"), 2455("PROG*", "ACL2", "COMMON-LISP"), 2456("REDUCE", "ACL2", "COMMON-LISP"), 2457("PROG1", "ACL2", "COMMON-LISP"), 2458("REINITIALIZE-INSTANCE", "ACL2", "COMMON-LISP"), 2459("PROG2", "ACL2", "COMMON-LISP"), 2460("REM", "ACL2", "COMMON-LISP"), 2461("PROGN", "ACL2", "COMMON-LISP"), 2462("REMF", "ACL2", "COMMON-LISP"), 2463("PROGRAM-ERROR", "ACL2", "COMMON-LISP"), 2464("REMHASH", "ACL2", "COMMON-LISP"), 2465("PROGV", "ACL2", "COMMON-LISP"), 2466("REMOVE", "ACL2", "COMMON-LISP"), 2467("PROVIDE", "ACL2", "COMMON-LISP"), 2468("REMOVE-DUPLICATES", "ACL2", "COMMON-LISP"), 2469("PSETF", "ACL2", "COMMON-LISP"), 2470("REMOVE-IF", "ACL2", "COMMON-LISP"), 2471("PSETQ", "ACL2", "COMMON-LISP"), 2472("REMOVE-IF-NOT", "ACL2", "COMMON-LISP"), 2473("PUSH", "ACL2", "COMMON-LISP"), 2474("REMOVE-METHOD", "ACL2", "COMMON-LISP"), 2475("PUSHNEW", "ACL2", "COMMON-LISP"), 2476("REMPROP", "ACL2", "COMMON-LISP"), 2477("QUOTE", "ACL2", "COMMON-LISP"), 2478("RENAME-FILE", "ACL2", "COMMON-LISP"), 2479("RANDOM", "ACL2", "COMMON-LISP"), 2480("RENAME-PACKAGE", "ACL2", "COMMON-LISP"), 2481("RANDOM-STATE", "ACL2", "COMMON-LISP"), 2482("REPLACE", "ACL2", "COMMON-LISP"), 2483("RANDOM-STATE-P", "ACL2", "COMMON-LISP"), 2484("REQUIRE", "ACL2", "COMMON-LISP"), 2485("RASSOC", "ACL2", "COMMON-LISP"), 2486("REST", "ACL2", "COMMON-LISP"), 2487("RASSOC-IF", "ACL2", "COMMON-LISP"), 2488("RESTART", "ACL2", "COMMON-LISP"), 2489("RASSOC-IF-NOT", "ACL2", "COMMON-LISP"), 2490("RESTART-BIND", "ACL2", "COMMON-LISP"), 2491("RATIO", "ACL2", "COMMON-LISP"), 2492("RESTART-CASE", "ACL2", "COMMON-LISP"), 2493("RATIONAL", "ACL2", "COMMON-LISP"), 2494("RESTART-NAME", "ACL2", "COMMON-LISP"), 2495("RATIONALIZE", "ACL2", "COMMON-LISP"), 2496("RETURN", "ACL2", "COMMON-LISP"), 2497("RATIONALP", "ACL2", "COMMON-LISP"), 2498("RETURN-FROM", "ACL2", "COMMON-LISP"), 2499("READ", "ACL2", "COMMON-LISP"), 2500("REVAPPEND", "ACL2", "COMMON-LISP"), 2501("READ-BYTE", "ACL2", "COMMON-LISP"), 2502("REVERSE", "ACL2", "COMMON-LISP"), 2503("ROOM", "ACL2", "COMMON-LISP"), 2504("SIMPLE-BIT-VECTOR", "ACL2", "COMMON-LISP"), 2505("ROTATEF", "ACL2", "COMMON-LISP"), 2506("SIMPLE-BIT-VECTOR-P", "ACL2", "COMMON-LISP"), 2507("ROUND", "ACL2", "COMMON-LISP"), 2508("SIMPLE-CONDITION", "ACL2", "COMMON-LISP"), 2509("ROW-MAJOR-AREF", "ACL2", "COMMON-LISP"), 2510("SIMPLE-CONDITION-FORMAT-ARGUMENTS", "ACL2", "COMMON-LISP"), 2511("RPLACA", "ACL2", "COMMON-LISP"), 2512("SIMPLE-CONDITION-FORMAT-CONTROL", "ACL2", "COMMON-LISP"), 2513("RPLACD", "ACL2", "COMMON-LISP"), 2514("SIMPLE-ERROR", "ACL2", "COMMON-LISP"), 2515("SAFETY", "ACL2", "COMMON-LISP"), 2516("SIMPLE-STRING", "ACL2", "COMMON-LISP"), 2517("SATISFIES", "ACL2", "COMMON-LISP"), 2518("SIMPLE-STRING-P", "ACL2", "COMMON-LISP"), 2519("SBIT", "ACL2", "COMMON-LISP"), 2520("SIMPLE-TYPE-ERROR", "ACL2", "COMMON-LISP"), 2521("SCALE-FLOAT", "ACL2", "COMMON-LISP"), 2522("SIMPLE-VECTOR", "ACL2", "COMMON-LISP"), 2523("SCHAR", "ACL2", "COMMON-LISP"), 2524("SIMPLE-VECTOR-P", "ACL2", "COMMON-LISP"), 2525("SEARCH", "ACL2", "COMMON-LISP"), 2526("SIMPLE-WARNING", "ACL2", "COMMON-LISP"), 2527("SECOND", "ACL2", "COMMON-LISP"), 2528("SIN", "ACL2", "COMMON-LISP"), 2529("SEQUENCE", "ACL2", "COMMON-LISP"), 2530("SINGLE-FLOAT", "ACL2", "COMMON-LISP"), 2531("SERIOUS-CONDITION", "ACL2", "COMMON-LISP"), 2532("SINGLE-FLOAT-EPSILON", "ACL2", "COMMON-LISP"), 2533("SET", "ACL2", "COMMON-LISP"), 2534("SINGLE-FLOAT-NEGATIVE-EPSILON", "ACL2", "COMMON-LISP"), 2535("SET-DIFFERENCE", "ACL2", "COMMON-LISP"), 2536("SINH", "ACL2", "COMMON-LISP"), 2537("SET-DISPATCH-MACRO-CHARACTER", "ACL2", "COMMON-LISP"), 2538("SIXTH", "ACL2", "COMMON-LISP"), 2539("SET-EXCLUSIVE-OR", "ACL2", "COMMON-LISP"), 2540("SLEEP", "ACL2", "COMMON-LISP"), 2541("SET-MACRO-CHARACTER", "ACL2", "COMMON-LISP"), 2542("SLOT-BOUNDP", "ACL2", "COMMON-LISP"), 2543("SET-PPRINT-DISPATCH", "ACL2", "COMMON-LISP"), 2544("SLOT-EXISTS-P", "ACL2", "COMMON-LISP"), 2545("SET-SYNTAX-FROM-CHAR", "ACL2", "COMMON-LISP"), 2546("SLOT-MAKUNBOUND", "ACL2", "COMMON-LISP"), 2547("SETF", "ACL2", "COMMON-LISP"), 2548("SLOT-MISSING", "ACL2", "COMMON-LISP"), 2549("SETQ", "ACL2", "COMMON-LISP"), 2550("SLOT-UNBOUND", "ACL2", "COMMON-LISP"), 2551("SEVENTH", "ACL2", "COMMON-LISP"), 2552("SLOT-VALUE", "ACL2", "COMMON-LISP"), 2553("SHADOW", "ACL2", "COMMON-LISP"), 2554("SOFTWARE-TYPE", "ACL2", "COMMON-LISP"), 2555("SHADOWING-IMPORT", "ACL2", "COMMON-LISP"), 2556("SOFTWARE-VERSION", "ACL2", "COMMON-LISP"), 2557("SHARED-INITIALIZE", "ACL2", "COMMON-LISP"), 2558("SOME", "ACL2", "COMMON-LISP"), 2559("SHIFTF", "ACL2", "COMMON-LISP"), 2560("SORT", "ACL2", "COMMON-LISP"), 2561("SHORT-FLOAT", "ACL2", "COMMON-LISP"), 2562("SPACE", "ACL2", "COMMON-LISP"), 2563("SHORT-FLOAT-EPSILON", "ACL2", "COMMON-LISP"), 2564("SPECIAL", "ACL2", "COMMON-LISP"), 2565("SHORT-FLOAT-NEGATIVE-EPSILON", "ACL2", "COMMON-LISP"), 2566("SPECIAL-OPERATOR-P", "ACL2", "COMMON-LISP"), 2567("SHORT-SITE-NAME", "ACL2", "COMMON-LISP"), 2568("SPEED", "ACL2", "COMMON-LISP"), 2569("SIGNAL", "ACL2", "COMMON-LISP"), 2570("SQRT", "ACL2", "COMMON-LISP"), 2571("SIGNED-BYTE", "ACL2", "COMMON-LISP"), 2572("STABLE-SORT", "ACL2", "COMMON-LISP"), 2573("SIGNUM", "ACL2", "COMMON-LISP"), 2574("STANDARD", "ACL2", "COMMON-LISP"), 2575("SIMPLE-ARRAY", "ACL2", "COMMON-LISP"), 2576("STANDARD-CHAR", "ACL2", "COMMON-LISP"), 2577("SIMPLE-BASE-STRING", "ACL2", "COMMON-LISP"), 2578("STANDARD-CHAR-P", "ACL2", "COMMON-LISP"), 2579("STANDARD-CLASS", "ACL2", "COMMON-LISP"), 2580("SUBLIS", "ACL2", "COMMON-LISP"), 2581("STANDARD-GENERIC-FUNCTION", "ACL2", "COMMON-LISP"), 2582("SUBSEQ", "ACL2", "COMMON-LISP"), 2583("STANDARD-METHOD", "ACL2", "COMMON-LISP"), 2584("SUBSETP", "ACL2", "COMMON-LISP"), 2585("STANDARD-OBJECT", "ACL2", "COMMON-LISP"), 2586("SUBST", "ACL2", "COMMON-LISP"), 2587("STEP", "ACL2", "COMMON-LISP"), 2588("SUBST-IF", "ACL2", "COMMON-LISP"), 2589("STORAGE-CONDITION", "ACL2", "COMMON-LISP"), 2590("SUBST-IF-NOT", "ACL2", "COMMON-LISP"), 2591("STORE-VALUE", "ACL2", "COMMON-LISP"), 2592("SUBSTITUTE", "ACL2", "COMMON-LISP"), 2593("STREAM", "ACL2", "COMMON-LISP"), 2594("SUBSTITUTE-IF", "ACL2", "COMMON-LISP"), 2595("STREAM-ELEMENT-TYPE", "ACL2", "COMMON-LISP"), 2596("SUBSTITUTE-IF-NOT", "ACL2", "COMMON-LISP"), 2597("STREAM-ERROR", "ACL2", "COMMON-LISP"), 2598("SUBTYPEP", "ACL2", "COMMON-LISP"), 2599("STREAM-ERROR-STREAM", "ACL2", "COMMON-LISP"), 2600("SVREF", "ACL2", "COMMON-LISP"), 2601("STREAM-EXTERNAL-FORMAT", "ACL2", "COMMON-LISP"), 2602("SXHASH", "ACL2", "COMMON-LISP"), 2603("STREAMP", "ACL2", "COMMON-LISP"), 2604("SYMBOL", "ACL2", "COMMON-LISP"), 2605("STRING", "ACL2", "COMMON-LISP"), 2606("SYMBOL-FUNCTION", "ACL2", "COMMON-LISP"), 2607("STRING-CAPITALIZE", "ACL2", "COMMON-LISP"), 2608("SYMBOL-MACROLET", "ACL2", "COMMON-LISP"), 2609("STRING-DOWNCASE", "ACL2", "COMMON-LISP"), 2610("SYMBOL-NAME", "ACL2", "COMMON-LISP"), 2611("STRING-EQUAL", "ACL2", "COMMON-LISP"), 2612("SYMBOL-PACKAGE", "ACL2", "COMMON-LISP"), 2613("STRING-GREATERP", "ACL2", "COMMON-LISP"), 2614("SYMBOL-PLIST", "ACL2", "COMMON-LISP"), 2615("STRING-LEFT-TRIM", "ACL2", "COMMON-LISP"), 2616("SYMBOL-VALUE", "ACL2", "COMMON-LISP"), 2617("STRING-LESSP", "ACL2", "COMMON-LISP"), 2618("SYMBOLP", "ACL2", "COMMON-LISP"), 2619("STRING-NOT-EQUAL", "ACL2", "COMMON-LISP"), 2620("SYNONYM-STREAM", "ACL2", "COMMON-LISP"), 2621("STRING-NOT-GREATERP", "ACL2", "COMMON-LISP"), 2622("SYNONYM-STREAM-SYMBOL", "ACL2", "COMMON-LISP"), 2623("STRING-NOT-LESSP", "ACL2", "COMMON-LISP"), 2624("T", "ACL2", "COMMON-LISP"), 2625("STRING-RIGHT-TRIM", "ACL2", "COMMON-LISP"), 2626("TAGBODY", "ACL2", "COMMON-LISP"), 2627("STRING-STREAM", "ACL2", "COMMON-LISP"), 2628("TAILP", "ACL2", "COMMON-LISP"), 2629("STRING-TRIM", "ACL2", "COMMON-LISP"), 2630("TAN", "ACL2", "COMMON-LISP"), 2631("STRING-UPCASE", "ACL2", "COMMON-LISP"), 2632("TANH", "ACL2", "COMMON-LISP"), 2633("STRING/=", "ACL2", "COMMON-LISP"), 2634("TENTH", "ACL2", "COMMON-LISP"), 2635("STRING<", "ACL2", "COMMON-LISP"), 2636("TERPRI", "ACL2", "COMMON-LISP"), 2637("STRING<=", "ACL2", "COMMON-LISP"), 2638("THE", "ACL2", "COMMON-LISP"), 2639("STRING=", "ACL2", "COMMON-LISP"), 2640("THIRD", "ACL2", "COMMON-LISP"), 2641("STRING>", "ACL2", "COMMON-LISP"), 2642("THROW", "ACL2", "COMMON-LISP"), 2643("STRING>=", "ACL2", "COMMON-LISP"), 2644("TIME", "ACL2", "COMMON-LISP"), 2645("STRINGP", "ACL2", "COMMON-LISP"), 2646("TRACE", "ACL2", "COMMON-LISP"), 2647("STRUCTURE", "ACL2", "COMMON-LISP"), 2648("TRANSLATE-LOGICAL-PATHNAME", "ACL2", "COMMON-LISP"), 2649("STRUCTURE-CLASS", "ACL2", "COMMON-LISP"), 2650("TRANSLATE-PATHNAME", "ACL2", "COMMON-LISP"), 2651("STRUCTURE-OBJECT", "ACL2", "COMMON-LISP"), 2652("TREE-EQUAL", "ACL2", "COMMON-LISP"), 2653("STYLE-WARNING", "ACL2", "COMMON-LISP"), 2654("TRUENAME", "ACL2", "COMMON-LISP"), 2655("TRUNCATE", "ACL2", "COMMON-LISP"), 2656("VALUES-LIST", "ACL2", "COMMON-LISP"), 2657("TWO-WAY-STREAM", "ACL2", "COMMON-LISP"), 2658("VARIABLE", "ACL2", "COMMON-LISP"), 2659("TWO-WAY-STREAM-INPUT-STREAM", "ACL2", "COMMON-LISP"), 2660("VECTOR", "ACL2", "COMMON-LISP"), 2661("TWO-WAY-STREAM-OUTPUT-STREAM", "ACL2", "COMMON-LISP"), 2662("VECTOR-POP", "ACL2", "COMMON-LISP"), 2663("TYPE", "ACL2", "COMMON-LISP"), 2664("VECTOR-PUSH", "ACL2", "COMMON-LISP"), 2665("TYPE-ERROR", "ACL2", "COMMON-LISP"), 2666("VECTOR-PUSH-EXTEND", "ACL2", "COMMON-LISP"), 2667("TYPE-ERROR-DATUM", "ACL2", "COMMON-LISP"), 2668("VECTORP", "ACL2", "COMMON-LISP"), 2669("TYPE-ERROR-EXPECTED-TYPE", "ACL2", "COMMON-LISP"), 2670("WARN", "ACL2", "COMMON-LISP"), 2671("TYPE-OF", "ACL2", "COMMON-LISP"), 2672("WARNING", "ACL2", "COMMON-LISP"), 2673("TYPECASE", "ACL2", "COMMON-LISP"), 2674("WHEN", "ACL2", "COMMON-LISP"), 2675("TYPEP", "ACL2", "COMMON-LISP"), 2676("WILD-PATHNAME-P", "ACL2", "COMMON-LISP"), 2677("UNBOUND-SLOT", "ACL2", "COMMON-LISP"), 2678("WITH-ACCESSORS", "ACL2", "COMMON-LISP"), 2679("UNBOUND-SLOT-INSTANCE", "ACL2", "COMMON-LISP"), 2680("WITH-COMPILATION-UNIT", "ACL2", "COMMON-LISP"), 2681("UNBOUND-VARIABLE", "ACL2", "COMMON-LISP"), 2682("WITH-CONDITION-RESTARTS", "ACL2", "COMMON-LISP"), 2683("UNDEFINED-FUNCTION", "ACL2", "COMMON-LISP"), 2684("WITH-HASH-TABLE-ITERATOR", "ACL2", "COMMON-LISP"), 2685("UNEXPORT", "ACL2", "COMMON-LISP"), 2686("WITH-INPUT-FROM-STRING", "ACL2", "COMMON-LISP"), 2687("UNINTERN", "ACL2", "COMMON-LISP"), 2688("WITH-OPEN-FILE", "ACL2", "COMMON-LISP"), 2689("UNION", "ACL2", "COMMON-LISP"), 2690("WITH-OPEN-STREAM", "ACL2", "COMMON-LISP"), 2691("UNLESS", "ACL2", "COMMON-LISP"), 2692("WITH-OUTPUT-TO-STRING", "ACL2", "COMMON-LISP"), 2693("UNREAD-CHAR", "ACL2", "COMMON-LISP"), 2694("WITH-PACKAGE-ITERATOR", "ACL2", "COMMON-LISP"), 2695("UNSIGNED-BYTE", "ACL2", "COMMON-LISP"), 2696("WITH-SIMPLE-RESTART", "ACL2", "COMMON-LISP"), 2697("UNTRACE", "ACL2", "COMMON-LISP"), 2698("WITH-SLOTS", "ACL2", "COMMON-LISP"), 2699("UNUSE-PACKAGE", "ACL2", "COMMON-LISP"), 2700("WITH-STANDARD-IO-SYNTAX", "ACL2", "COMMON-LISP"), 2701("UNWIND-PROTECT", "ACL2", "COMMON-LISP"), 2702("WRITE", "ACL2", "COMMON-LISP"), 2703("UPDATE-INSTANCE-FOR-DIFFERENT-CLASS", "ACL2", "COMMON-LISP"), 2704("WRITE-BYTE", "ACL2", "COMMON-LISP"), 2705("UPDATE-INSTANCE-FOR-REDEFINED-CLASS", "ACL2", "COMMON-LISP"), 2706("WRITE-CHAR", "ACL2", "COMMON-LISP"), 2707("UPGRADED-ARRAY-ELEMENT-TYPE", "ACL2", "COMMON-LISP"), 2708("WRITE-LINE", "ACL2", "COMMON-LISP"), 2709("UPGRADED-COMPLEX-PART-TYPE", "ACL2", "COMMON-LISP"), 2710("WRITE-SEQUENCE", "ACL2", "COMMON-LISP"), 2711("UPPER-CASE-P", "ACL2", "COMMON-LISP"), 2712("WRITE-STRING", "ACL2", "COMMON-LISP"), 2713("USE-PACKAGE", "ACL2", "COMMON-LISP"), 2714("WRITE-TO-STRING", "ACL2", "COMMON-LISP"), 2715("USE-VALUE", "ACL2", "COMMON-LISP"), 2716("Y-OR-N-P", "ACL2", "COMMON-LISP"), 2717("USER-HOMEDIR-PATHNAME", "ACL2", "COMMON-LISP"), 2718("YES-OR-NO-P", "ACL2", "COMMON-LISP"), 2719("VALUES", "ACL2", "COMMON-LISP"), 2720("ZEROP", "ACL2", "COMMON-LISP") 2721] 2722