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