; ACL2 Version 8.0 -- A Computational Logic for Applicative Common Lisp
; Copyright (C) 2017, Regents of the University of Texas

; This version of ACL2 is a descendent of ACL2 Version 1.9, Copyright
; (C) 1997 Computational Logic, Inc.  See the documentation topic NOTE-2-0.

; This program is free software; you can redistribute it and/or modify
; it under the terms of the LICENSE file distributed with ACL2.

; This program is distributed in the hope that it will be useful,
; but WITHOUT ANY WARRANTY; without even the implied warranty of
; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
; LICENSE for more details.

; Written by:  Matt Kaufmann               and J Strother Moore
; email:       Kaufmann@cs.utexas.edu      and Moore@cs.utexas.edu
; Department of Computer Science
; University of Texas at Austin
; Austin, TX 78712 U.S.A.

; This file, defpkgs.lisp, illustrates the idea that defpkg forms
; should be off in files all by themselves.  We require defpkg forms
; to be in files all by themselves to support the compilation of
; files.  Files with defpkg forms should only be loaded, never
; compiled.  Of course, during the compilation of other files, it will
; be necessary for defpkg files to be loaded at the appropriate time.
; The idea of putting defpkg forms in separate files is in the spirit
; of the CLTL2 idea of putting DEFPACKAGE forms in separate files.  By
; keeping package creation separate from compilation, one avoids many
; pitfalls and inconsistencies between Common Lisp implementations.

(in-package "ACL2")

(defconst *acl2-exports*

; This constant provides a handy list of symbols to export from the ACL2
; package.  The goal is to make it easy for ACL2 users to import documented
; symbols into their own packages, by importing *acl2-exports* (and probably
; also *common-lisp-symbols-from-main-lisp-package*).  This list thus includes
; all documented constants, functions, and macros, except for those that we
; explicitly exclude, as checked by certifying community book
; books/misc/check-acl2-exports.lisp.  See that book for the list of symbols,
; *acl2-exports-exclusions*, that we explicitly exclude from the requirement
; that documented constants, functions, and macros must belong to
; *acl2-exports*.

; WARNING: When you document a new constant, function, or macro symbol defined
; by ACL2, then you MUST either add that symbol to *acl2-exports* or else add
; it to the constant *acl2-exports-exclusions* in community book
; books/misc/check-acl2-exports.lisp.  (See the preceding paragraph for
; relevant remarks.)  Otherwise, after you rebuild doc.lisp (for example using
; "make DOC") and then rebuild an ACL2 executable, certification will likely
; fail with that executable for books/misc/check-acl2-exports.lisp.  (Note that
; there is NOT such a failure in regression testing based on an executable that
; was built before updating doc.lisp, as has long been typical as of this
; writing in May 2017.)  It is ultimately best in most cases to add the symbol
; to *acl2-exports* rather than to *acl2-exports-exclusions*; but for github
; versions between releases it can be polite to add it temporarily to
; *acl2-exports-exclusions*, so that package definitions aren't affected
; (otherwise git users who update may need to recertify many books).  There
; should be a comment in that constant definition, saying "Symbols below should
; probably be added to *acl2-exports*", indicating where to add such a symbol.

; We keep this list sorted, since that makes defpkg more efficient when users
; choose to import these symbols; it avoids having to sort them then.

  (sort-symbol-listp
   (append
    *hons-primitives* ; even for non-hons version, for compatibility of the two
    '(TRACE* ; not defined by ACL2, but may well be defined in a book
      GRANULARITY ; for parallelism primitives
      )
    '(& &ALLOW-OTHER-KEYS &AUX &BODY &KEY
        &OPTIONAL &REST &WHOLE * *ACL2-EXPORTS*
        *COMMON-LISP-SPECIALS-AND-CONSTANTS*
        *COMMON-LISP-SYMBOLS-FROM-MAIN-LISP-PACKAGE*
        *MAIN-LISP-PACKAGE-NAME*
        *STANDARD-CHARS* *STANDARD-CI*
        *STANDARD-CO* *STANDARD-OI*
        + - / /= 1+ 1- 32-BIT-INTEGER-LISTP
        32-BIT-INTEGER-LISTP-FORWARD-TO-INTEGER-LISTP
        32-BIT-INTEGER-STACK
        32-BIT-INTEGER-STACK-LENGTH
        32-BIT-INTEGER-STACK-LENGTH1
        32-BIT-INTEGERP
        32-BIT-INTEGERP-FORWARD-TO-INTEGERP
        < <-ON-OTHERS <= = > >= ?-FN @ A! ABORT!
        ABS ACCESS ACCUMULATED-PERSISTENCE ACCUMULATED-PERSISTENCE-OOPS
        ACL2-COUNT
        ACL2-INPUT-CHANNEL-PACKAGE ACL2-NUMBER-LISTP ACL2-NUMBERP
        ACL2-ORACLE ACL2-OUTPUT-CHANNEL-PACKAGE
        ACL2-PACKAGE ACONS ACTIVE-OR-NON-RUNEP ACTIVE-RUNEP
        ADD-BINOP ADD-CUSTOM-KEYWORD-HINT
        ADD-DEFAULT-HINTS ADD-DEFAULT-HINTS!
        ADD-INCLUDE-BOOK-DIR ADD-INCLUDE-BOOK-DIR!
        ADD-INVISIBLE-FNS ADD-LD-KEYWORD-ALIAS ADD-LD-KEYWORD-ALIAS!
        ADD-MACRO-ALIAS ADD-MACRO-FN
        ADD-MATCH-FREE-OVERRIDE ADD-NTH-ALIAS
        ADD-OVERRIDE-HINTS ADD-OVERRIDE-HINTS!
        ADD-PAIR ADD-PAIR-PRESERVES-ALL-BOUNDP
        ADD-RAW-ARITY ADD-TIMERS ADD-TO-SET ADD-TO-SET-EQ
        ADD-TO-SET-EQL ADD-TO-SET-EQUAL
        ALISTP ALISTP-FORWARD-TO-TRUE-LISTP
        ALL-BOUNDP ALL-BOUNDP-PRESERVES-ASSOC
        ALL-VARS ALL-VARS1 ALL-VARS1-LST
        ALLOCATE-FIXNUM-RANGE ALPHA-CHAR-P
        ALPHA-CHAR-P-FORWARD-TO-CHARACTERP
        ALPHORDER AND AND-MACRO APPEND APPLY$
        AREF-32-BIT-INTEGER-STACK AREF-T-STACK
        AREF1 AREF2 ARGS ARITIES-OKP ARITY ARRAY1P ARRAY1P-CONS
        ARRAY1P-FORWARD ARRAY1P-LINEAR
        ARRAY2P ARRAY2P-CONS ARRAY2P-FORWARD
        ARRAY2P-LINEAR ASET-32-BIT-INTEGER-STACK
        ASET-T-STACK ASET1 ASET2
        ASH ASSERT$ ASSERT* ASSERT-EVENT ASSIGN ASSOC
        ASSOC-ADD-PAIR ASSOC-EQ ASSOC-EQ-EQUAL
        ASSOC-EQ-EQUAL-ALISTP ASSOC-EQUAL
        ASSOC-KEYWORD ASSOC-STRING-EQUAL ASSOC2
        ASSOCIATIVITY-OF-* ASSOCIATIVITY-OF-+
        ASSUME ATOM ATOM-LISTP
        ATOM-LISTP-FORWARD-TO-TRUE-LISTP
        BACKCHAIN-LIMIT BIG-CLOCK-ENTRY
        BIG-CLOCK-NEGATIVE-P BINARY-*
        BINARY-+ BINARY-APPEND BIND-FREE
        BIT BITP BOOLE$ BOOLEAN-LISTP
        BOOLEAN-LISTP-CONS BOOLEAN-LISTP-FORWARD
        BOOLEAN-LISTP-FORWARD-TO-SYMBOL-LISTP
        BOOLEANP BOOLEANP-CHARACTERP
        BOOLEANP-COMPOUND-RECOGNIZER
        BOUNDED-INTEGER-ALISTP
        BOUNDED-INTEGER-ALISTP-FORWARD-TO-EQLABLE-ALISTP
        BOUNDED-INTEGER-ALISTP2 BOUNDP-GLOBAL
        BOUNDP-GLOBAL1 BREAK$ BREAK-ON-ERROR
        BRR BRR@ BUILD-STATE1 BUTLAST
        CAAAAR CAAADR CAAAR CAADAR CAADDR
        CAADR CAAR CADAAR CADADR CADAR CADDAR
        CADDDR CADDR CADR CANONICAL-PATHNAME
        CAR CAR-CDR-ELIM CAR-CONS CASE
        CASE-LIST CASE-LIST-CHECK CASE-MATCH
        CASE-SPLIT CASE-SPLIT-LIMITATIONS
        CASE-TEST CBD CDAAAR CDAADR
        CDAAR CDADAR CDADDR CDADR CDAR CDDAAR
        CDDADR CDDAR CDDDAR CDDDDR CDDDR CDDR
        CDR CDR-CONS CDRN CEILING CERTIFY-BOOK
        CERTIFY-BOOK! CHANGE CHAR CHAR-CODE
        CHAR-CODE-CODE-CHAR-IS-IDENTITY
        CHAR-CODE-LINEAR CHAR-DOWNCASE
        CHAR-EQUAL CHAR-UPCASE CHAR< CHAR<=
        CHAR> CHAR>= CHARACTER CHARACTER-ALISTP
        CHARACTER-LISTP CHARACTER-LISTP-APPEND
        CHARACTER-LISTP-COERCE
        CHARACTER-LISTP-FORWARD-TO-EQLABLE-LISTP
        CHARACTER-LISTP-REMOVE-DUPLICATES-EQL
        CHARACTER-LISTP-REVAPPEND
        CHARACTER-LISTP-STRING-DOWNCASE-1
        CHARACTER-LISTP-STRING-UPCASE1-1
        CHARACTERP CHARACTERP-CHAR-DOWNCASE
        CHARACTERP-CHAR-UPCASE CHARACTERP-NTH
        CHARACTERP-PAGE CHARACTERP-RUBOUT CHARACTERP-RETURN
        CHARACTERP-TAB CHECK-INVARIANT-RISK CHECK-VARS-NOT-FREE
        CHECKPOINT-FORCED-GOALS CHECKPOINT-SUMMARY-LIMIT CLAUSE
        CLOSE-INPUT-CHANNEL CLOSE-OUTPUT-CHANNEL
        CLOSE-TRACE-FILE CLOSURE CODE-CHAR
        CODE-CHAR-CHAR-CODE-IS-IDENTITY
        CODE-CHAR-TYPE COERCE COERCE-INVERSE-1
        COERCE-INVERSE-2 COERCE-OBJECT-TO-STATE
        COERCE-STATE-TO-OBJECT
        COMMUNITY-BOOKS
        COMMUTATIVITY-OF-*
        COMMUTATIVITY-OF-+ COMP COMPLETION-OF-*
        COMPLETION-OF-+ COMPLETION-OF-<
        COMPLETION-OF-CAR COMPLETION-OF-CDR
        COMPLETION-OF-CHAR-CODE
        COMPLETION-OF-CODE-CHAR
        COMPLETION-OF-COERCE
        COMPLETION-OF-COMPLEX
        COMPLETION-OF-DENOMINATOR
        COMPLETION-OF-IMAGPART
        COMPLETION-OF-INTERN-IN-PACKAGE-OF-SYMBOL
        COMPLETION-OF-NUMERATOR
        COMPLETION-OF-REALPART
        COMPLETION-OF-SYMBOL-NAME
        COMPLETION-OF-SYMBOL-PACKAGE-NAME
        COMPLETION-OF-UNARY-/
        COMPLETION-OF-UNARY-MINUS
        COMPLEX COMPLEX-0
        COMPLEX-DEFINITION COMPLEX-EQUAL
        COMPLEX-IMPLIES1 COMPLEX-RATIONALP
        COMPLEX/COMPLEX-RATIONALP
        COMPRESS1 COMPRESS11 COMPRESS2
        COMPRESS21 COMPRESS211 CONCATENATE
        CONCRETE-BADGE-USERFN CONCRETE-APPLY$-USERFN
        COND COND-CLAUSESP COND-MACRO
        CONJUGATE CONS CONS-EQUAL CONS-WITH-HINT CONSP
        CONSP-ASSOC-EQUAL CONSTRAINT-INFO COROLLARY CPU-CORE-COUNT
        CTX ; perhaps useful for computed hints
        CURRENT-PACKAGE CURRENT-THEORY CW CW! CW-GSTACK DECLARE
        DECREMENT-BIG-CLOCK DEFABBREV DEFABSSTOBJ
        DEFABSSTOBJ-MISSING-EVENTS DEFATTACH
        DEFAULT DEFAULT-*-1 DEFAULT-*-2
        DEFAULT-+-1 DEFAULT-+-2 DEFAULT-<-1
        DEFAULT-<-2 DEFAULT-BACKCHAIN-LIMIT
        DEFAULT-CAR DEFAULT-CDR
        DEFAULT-CHAR-CODE DEFAULT-COERCE-1
        DEFAULT-COERCE-2 DEFAULT-COERCE-3
        DEFAULT-COMPILE-FNS DEFAULT-COMPLEX-1
        DEFAULT-COMPLEX-2 DEFAULT-DEFUN-MODE
        DEFAULT-DEFUN-MODE-FROM-STATE
        DEFAULT-DENOMINATOR
        DEFAULT-HINTS DEFAULT-IMAGPART
        DEFAULT-MEASURE-FUNCTION
        DEFAULT-NUMERATOR
        DEFAULT-PRINT-PROMPT DEFAULT-REALPART DEFAULT-RULER-EXTENDERS
        DEFAULT-STATE-VARS DEFAULT-SYMBOL-NAME
        DEFAULT-SYMBOL-PACKAGE-NAME DEFAULT-TOTAL-PARALLELISM-WORK-LIMIT
        DEFAULT-UNARY-/ DEFAULT-UNARY-MINUS
        DEFAULT-VERIFY-GUARDS-EAGERNESS
        DEFAULT-WELL-FOUNDED-RELATION
        DEFAXIOM DEFCHOOSE DEFCONG DEFCONST
        DEFEQUIV DEFEVALUATOR DEFEXEC
        DEFINE-PC-ATOMIC-MACRO DEFINE-PC-HELP
        DEFINE-PC-MACRO DEFINE-PC-META
        DEFINE-TRUSTED-CLAUSE-PROCESSOR
        DEFLABEL DEFLOCK DEFMACRO DEFMACRO-LAST DEFN DEFND DEFPKG
        DEFPROXY DEFREC DEFREFINEMENT DEFSTOBJ DEFSTUB
        DEFTHEORY DEFTHEORY-STATIC
        DEFTHM DEFTHMD DEFTHY DEFTTAG
        DEFUN DEFUN-INLINE DEFUN-NOTINLINE DEFUN-NX
        DEFUN-SK DEFUND DEFUND-INLINE DEFUND-NOTINLINE DEFUND-NX DEFUNS
        DELETE-ASSOC DELETE-ASSOC-EQ DELETE-ASSOC-EQUAL DELETE-FILE$
        DELETE-INCLUDE-BOOK-DIR DELETE-INCLUDE-BOOK-DIR!
        DENOMINATOR DIGIT-CHAR-P DIGIT-TO-CHAR
        DIMENSIONS DISABLE DISABLE-FORCING
        DISABLE-IMMEDIATE-FORCE-MODEP
        DISABLEDP DISASSEMBLE$ DISTRIBUTIVITY
        DMR-START DMR-STOP DOC DOC! DOCS DOUBLE-REWRITE
        DUPLICATES E/D E0-ORD-< E0-ORDINALP
        EC-CALL EIGHTH ELIMINATE-DESTRUCTORS
        ELIMINATE-IRRELEVANCE
        ENABLE ENABLE-FORCING
        ENABLE-IMMEDIATE-FORCE-MODEP
        ENCAPSULATE ENDP EQ EQL EQLABLE-ALISTP
        EQLABLE-ALISTP-FORWARD-TO-ALISTP
        EQLABLE-LISTP
        EQLABLE-LISTP-FORWARD-TO-ATOM-LISTP
        EQLABLEP EQLABLEP-RECOG EQUAL
        EQUAL-CHAR-CODE ER ER-LET* ER-PROGN ER-PROGN-FN
        ER-PROGN-FN@PAR ER-PROGN@PAR ER-SOFT-LOGIC
        EV$ EV$-LIST EVENP EVENS EVENT EVISC-TUPLE
        EXECUTABLE-COUNTERPART-THEORY
        EXISTS EXIT EXPLODE-ATOM
        EXPLODE-NONNEGATIVE-INTEGER EXPT
        EXPT-TYPE-PRESCRIPTION-NON-ZERO-BASE
        EXTEND-32-BIT-INTEGER-STACK
        EXTEND-PE-TABLE EXTEND-T-STACK
        EXTEND-WORLD EXTRA-INFO F-GET-GLOBAL F-PUT-GLOBAL
        FAST-ALIST-CLEAN FAST-ALIST-CLEAN! FAST-ALIST-FORK FAST-ALIST-FORK!
        FAST-ALIST-FREE-ON-EXIT FC-REPORT FERTILIZE
        FGETPROP FIFTH FILE-CLOCK FILE-CLOCK-P
        FILE-CLOCK-P-FORWARD-TO-INTEGERP FILE-LENGTH$ FILE-WRITE-DATE$
        FINALIZE-EVENT-USER
        FIRST FIRST-N-AC
        FIX FIX-TRUE-LIST FLET FLOOR FLUSH-COMPRESS
        FMS FMS!
        FMS!-TO-STRING FMS-TO-STRING
        FMT FMT! FMT!-TO-STRING
        FMT-TO-COMMENT-WINDOW FMT-TO-STRING FMT1 FMT1!
        FMT1!-TO-STRING FMT1-TO-STRING
        FNCALL-TERM FORALL FORCE FORMULA FOURTH FUNCTION-SYMBOLP
        FUNCTION-THEORY GAG-MODE GC$
        GC-STRATEGY GC-VERBOSE GCS GENERALIZE
        GET-CHECK-INVARIANT-RISK GET-COMMAND-SEQUENCE GET-ENFORCE-REDUNDANCY
        GET-EVENT-DATA GET-GLOBAL GET-OUTPUT-STREAM-STRING$
        GET-REGISTER-INVARIANT-RISK GET-TIMER GET-WORMHOLE-STATUS
        GETENV$ GETPROP GETPROP-DEFAULT GETPROPC GETPROPS
        GETPROPS1 GLOBAL-TABLE GLOBAL-TABLE-CARS
        GLOBAL-TABLE-CARS1 GLOBAL-VAL
        GOOD-ATOM-LISTP GOOD-BYE GROUND-ZERO GTHM
        GUARD GUARD-OBLIGATION GUARD-THEOREM HARD-ERROR
        HAS-PROPSP HAS-PROPSP1 HEADER HELP HIDE
        HIST ; for computed hints
        HONS-ASSOC-EQUAL HONS-COPY-PERSISTENT
        HONS-SHRINK-ALIST HONS-SHRINK-ALIST!
        I-AM-HERE ID IDATES IDENTITY
        IF IF* IFF IFF-IMPLIES-EQUAL-IMPLIES-1
        IFF-IMPLIES-EQUAL-IMPLIES-2
        IFF-IMPLIES-EQUAL-NOT
        IFF-IS-AN-EQUIVALENCE IFIX
        IGNORABLE IGNORE ILLEGAL IMAGPART IMAGPART-COMPLEX
        IMMEDIATE-FORCE-MODEP IMPLIES
        IMPROPER-CONSP IN-ARITHMETIC-THEORY
        IN-PACKAGE IN-TAU-INTERVALP IN-THEORY INCLUDE-BOOK
        INCOMPATIBLE INCOMPATIBLE! INCREMENT-TIMER
        INDUCT INITIALIZE-EVENT-USER INT= INTEGER INTEGER-0 INTEGER-1
        INTEGER-ABS INTEGER-IMPLIES-RATIONAL
        INTEGER-LENGTH INTEGER-LISTP
        INTEGER-LISTP-FORWARD-TO-RATIONAL-LISTP
        INTEGER-RANGE-P INTEGER-STEP INTEGERP INTERN
        INTERN$ INTERN-IN-PACKAGE-OF-SYMBOL
        INTERN-IN-PACKAGE-OF-SYMBOL-SYMBOL-NAME
        INTERSECTION$ INTERSECTION-EQ
        INTERSECTION-EQUAL INTERSECTION-THEORIES
        INTERSECTP INTERSECTP-EQ
        INTERSECTP-EQUAL INVERSE-OF-*
        INVERSE-OF-+ INVISIBLE-FNS-TABLE
        IRRELEVANT
        KEYWORD-PACKAGE KEYWORD-VALUE-LISTP
        KEYWORD-VALUE-LISTP-ASSOC-KEYWORD
        KEYWORD-VALUE-LISTP-FORWARD-TO-TRUE-LISTP
        KEYWORDP KEYWORDP-FORWARD-TO-SYMBOLP
        KNOWN-PACKAGE-ALIST KNOWN-PACKAGE-ALISTP
        KNOWN-PACKAGE-ALISTP-FORWARD-TO-TRUE-LIST-LISTP-AND-ALISTP
        KWOTE
        KWOTE-LST LAMBDA LAST LAST-PROVER-STEPS LD LD-ERROR-ACTION
        LD-ERROR-TRIPLES LD-EVISC-TUPLE
        LD-KEYWORD-ALIASES LD-MISSING-INPUT-OK LD-POST-EVAL-PRINT
        LD-PRE-EVAL-FILTER LD-PRE-EVAL-PRINT
        LD-PROMPT LD-QUERY-CONTROL-ALIST
        LD-REDEFINITION-ACTION LD-SKIP-PROOFSP
        LD-VERBOSE LEGAL-CASE-CLAUSESP LEN
        LEN-UPDATE-NTH LENGTH LET LET* LET-MBE LEXORDER LIST
        LIST* LIST*-MACRO LIST-ALL-PACKAGE-NAMES
        LIST-ALL-PACKAGE-NAMES-LST
        LIST-MACRO LISTP LOCAL LOGAND
        LOGANDC1 LOGANDC2 LOGBITP LOGCOUNT
        LOGEQV LOGIC
        LOGIC-FNS-LIST-LISTP LOGIC-FNS-LISTP LOGIC-FNSP
        LOGIC-TERM-LIST-LISTP LOGIC-TERM-LISTP LOGIC-TERMP
        LOGIOR LOGNAND LOGNOR
        LOGNOT LOGORC1 LOGORC2 LOGTEST LOGXOR
        LOWER-CASE-P LOWER-CASE-P-CHAR-DOWNCASE
        LOWER-CASE-P-FORWARD-TO-ALPHA-CHAR-P
        LOWEST-TERMS LP MACRO-ALIASES MACRO-ARGS
        MAGIC-EV-FNCALL
        MAIN-TIMER MAIN-TIMER-TYPE-PRESCRIPTION
        MAKE MAKE-CHARACTER-LIST
        MAKE-CHARACTER-LIST-MAKE-CHARACTER-LIST
        MAKE-EVENT MAKE-FAST-ALIST
        MAKE-FMT-BINDINGS MAKE-INPUT-CHANNEL
        MAKE-LIST MAKE-LIST-AC MAKE-MV-NTHS
        MAKE-ORD MAKE-OUTPUT-CHANNEL
        MAKE-TAU-INTERVAL
        MAKE-VAR-LST MAKE-VAR-LST1
        MAKE-WORMHOLE-STATUS MAKUNBOUND-GLOBAL
        MAX MAXIMUM-LENGTH MAY-NEED-SLASHES
        MBE MBT MBT*
        MEMBER MEMBER-EQ MEMBER-EQUAL MEMBER-SYMBOL-NAME
        META-EXTRACT-CONTEXTUAL-FACT META-EXTRACT-FORMULA
        META-EXTRACT-GLOBAL-FACT META-EXTRACT-GLOBAL-FACT+ META-EXTRACT-RW+-TERM
        MFC
        MFC-ANCESTORS MFC-AP MFC-CLAUSE MFC-RDEPTH MFC-RELIEVE-HYP MFC-RW
        MFC-RW+ MFC-TS MFC-TYPE-ALIST MFC-UNIFY-SUBST MFC-WORLD
        MIN MINIMAL-THEORY MINUSP
        MOD MOD-EXPT MONITOR MONITORED-RUNES
        MORE MORE! MORE-DOC MSG MSGP MUST-BE-EQUAL
        MUTUAL-RECURSION MUTUAL-RECURSION-GUARDP
        MV MV-LET MV-LIST MV-NTH MV? MV?-LET
        NAT-LISTP NATP NEAR-MISSES NEEDS-SLASHES NEVER-MEMOIZE NEWLINE
        NFIX NIL NIL-IS-NOT-CIRCULAR NINTH
        NO-DUPLICATESP NO-DUPLICATESP-EQ NO-DUPLICATESP-EQUAL
        NON-EXEC NONNEGATIVE-INTEGER-QUOTIENT
        NONNEGATIVE-PRODUCT NONZERO-IMAGPART
        NOT NQTHM-TO-ACL2 NTH NTH-0-CONS
        NTH-0-READ-RUN-TIME-TYPE-PRESCRIPTION
        NTH-ADD1
        NTH-ALIASES NTH-UPDATE-NTH NTHCDR
        NULL NUMERATOR O-FINP O-FIRST-COEFF
        O-FIRST-EXPT O-INFP O-P O-RST O<
        O<= O> O>= OBSERVATION OBSERVATION-CW ODDP ODDS OK-IF
        OOPS OPEN-CHANNEL-LISTP OPEN-CHANNEL1
        OPEN-CHANNEL1-FORWARD-TO-TRUE-LISTP-AND-CONSP
        OPEN-CHANNELS-P OPEN-CHANNELS-P-FORWARD
        OPEN-INPUT-CHANNEL
        OPEN-INPUT-CHANNEL-ANY-P
        OPEN-INPUT-CHANNEL-ANY-P1
        OPEN-INPUT-CHANNEL-P
        OPEN-INPUT-CHANNEL-P1
        OPEN-INPUT-CHANNELS
        OPEN-OUTPUT-CHANNEL OPEN-OUTPUT-CHANNEL!
        OPEN-OUTPUT-CHANNEL-ANY-P
        OPEN-OUTPUT-CHANNEL-ANY-P1
        OPEN-OUTPUT-CHANNEL-P
        OPEN-OUTPUT-CHANNEL-P1
        OPEN-OUTPUT-CHANNELS OPEN-TRACE-FILE
        OPTIMIZE
        OR OR-MACRO
        ORDERED-SYMBOL-ALISTP
        ORDERED-SYMBOL-ALISTP-ADD-PAIR
        ORDERED-SYMBOL-ALISTP-ADD-PAIR-FORWARD
        ORDERED-SYMBOL-ALISTP-DELETE-ASSOC-EQ
        ORDERED-SYMBOL-ALISTP-FORWARD-TO-SYMBOL-ALISTP
        ORDERED-SYMBOL-ALISTP-GETPROPS
        OTHERWISE
        OUR-DIGIT-CHAR-P OVERRIDE-HINTS
        P! PAIRLIS$ PAIRLIS2 PAND PARGS
        PBT PC PCB PCB! PCS PE PE! PEEK-CHAR$
        PF PKG-IMPORTS PKG-WITNESS PL PL2 PLET PLIST-WORLDP
        PLIST-WORLDP-FORWARD-TO-ASSOC-EQ-EQUAL-ALISTP
        PLUSP
        POINTERS ; so that XDOC::POINTERS is ACL2::POINTERS
        POP-TIMER POR POSITION
        POSITION-AC POSITION-EQ POSITION-EQ-AC
        POSITION-EQUAL POSITION-EQUAL-AC
        POSITIVE POSP POWER-EVAL PPROGN PR
        PR! PREPROCESS PRIN1$ PRIN1-WITH-SLASHES
        PRIN1-WITH-SLASHES1 PRINC$ PRINT-BASE-P PRINT-GV
        PRINT-OBJECT$ PRINT-OBJECT$-PRESERVING-CASE PRINT-OBJECT$-SER
        PRINT-RATIONAL-AS-DECIMAL
        PRINT-TIMER PROFILE
        PROG2$ PROGN PROGN! PROGN$ PROGRAM
        PROOF-TREE PROOFS-CO PROPER-CONSP
        PROPS PROVE PSEUDO-TERM-LISTP
        PSEUDO-TERM-LISTP-FORWARD-TO-TRUE-LISTP
        PSEUDO-TERMP PSO PSO! PSOF PSOG
        PSPV ; for computed hints
        PSTACK PUFF PUFF* PUSH-TIMER PUSH-UNTOUCHABLE
        PUT-ASSOC PUT-ASSOC-EQ PUT-ASSOC-EQL
        PUT-ASSOC-EQUAL PUT-GLOBAL PUTPROP
        QUICK-AND-DIRTY-SUBSUMPTION-REPLACEMENT-STEP
        QUIT QUOTE QUOTEP R-EQLABLE-ALISTP R-SYMBOL-ALISTP
        RANDOM$ RASSOC RASSOC-EQ RASSOC-EQUAL
        RATIO RATIONAL RATIONAL-IMPLIES1
        RATIONAL-IMPLIES2 RATIONAL-LISTP
        RATIONAL-LISTP-FORWARD-TO-TRUE-LISTP
        RATIONALP RATIONALP-* RATIONALP-+
        RATIONALP-EXPT-TYPE-PRESCRIPTION
        RATIONALP-IMPLIES-ACL2-NUMBERP
        RATIONALP-UNARY--
        RATIONALP-UNARY-/ READ-ACL2-ORACLE
        READ-ACL2-ORACLE-PRESERVES-STATE-P1
        READ-BYTE$ READ-CHAR$ READ-FILE-INTO-STRING READ-FILE-LISTP
        READ-FILE-LISTP-FORWARD-TO-TRUE-LIST-LISTP
        READ-FILE-LISTP1
        READ-FILE-LISTP1-FORWARD-TO-TRUE-LISTP-AND-CONSP
        READ-FILES READ-FILES-P
        READ-FILES-P-FORWARD-TO-READ-FILE-LISTP
        READ-IDATE READ-OBJECT READ-OBJECT-SUPPRESS READ-OBJECT-WITH-CASE
        READ-RUN-TIME READ-RUN-TIME-PRESERVES-STATE-P1
        READABLE-FILE
        READABLE-FILE-FORWARD-TO-TRUE-LISTP-AND-CONSP
        READABLE-FILES READABLE-FILES-LISTP
        READABLE-FILES-LISTP-FORWARD-TO-TRUE-LIST-LISTP-AND-ALISTP
        READABLE-FILES-P
        READABLE-FILES-P-FORWARD-TO-READABLE-FILES-LISTP
        REAL/RATIONALP REALFIX REALPART
        REALPART-COMPLEX REALPART-IMAGPART-ELIM
        REBUILD REDEF REDEF!
        REDEF+ REDEF- REDO-FLAT
        REGENERATE-TAU-DATABASE
        REM REMOVE
        REMOVE-BINOP REMOVE-CUSTOM-KEYWORD-HINT
        REMOVE-DEFAULT-HINTS
        REMOVE-DEFAULT-HINTS!
        REMOVE-DUPLICATES REMOVE-DUPLICATES-EQ REMOVE-DUPLICATES-EQL
        REMOVE-DUPLICATES-EQUAL
        REMOVE-EQ REMOVE-EQUAL REMOVE-GUARD-HOLDERS
        REMOVE-INVISIBLE-FNS REMOVE-MACRO-ALIAS REMOVE-MACRO-FN
        REMOVE-NTH-ALIAS REMOVE-OVERRIDE-HINTS
        REMOVE-OVERRIDE-HINTS!
        REMOVE-RAW-ARITY REMOVE-UNTOUCHABLE
        REMOVE1 REMOVE1-EQ REMOVE1-EQUAL RESET-FC-REPORTING
        RESET-KILL-RING RESET-LD-SPECIALS
        RESET-PREHISTORY RESET-PRINT-CONTROL
        RESIZE-LIST REST RESTORE-MEMOIZATION-SETTINGS RETRACT-WORLD
        RETRIEVE RETURN-LAST RETURN-LAST-TABLE
        REVAPPEND REVERSE REVERT-WORLD REWRITE-STACK-LIMIT
        RFIX ROUND RW-CACHE SATISFIES
        SAVE-AND-CLEAR-MEMOIZATION-SETTINGS SAVE-EXEC
        SEARCH SECOND
        SERIALIZE-READ SERIALIZE-WRITE SET-ABSSTOBJ-DEBUG
        SET-ACCUMULATED-PERSISTENCE
        SET-BACKCHAIN-LIMIT SET-BAD-LISP-CONSP-MEMOIZE
        SET-BODY SET-BOGUS-DEFUN-HINTS-OK SET-BOGUS-MEASURE-OK
        SET-BOGUS-MUTUAL-RECURSION-OK
        SET-CASE-SPLIT-LIMITATIONS
        SET-CBD
        SET-CHECK-INVARIANT-RISK
        SET-CHECKPOINT-SUMMARY-LIMIT
        SET-COMPILE-FNS
        SET-COMPILER-ENABLED SET-DEBUGGER-ENABLE
        SET-DEFAULT-BACKCHAIN-LIMIT
        SET-DEFAULT-HINTS SET-DEFAULT-HINTS!
        SET-DEFERRED-TTAG-NOTES
        SET-DIFFERENCE$ SET-DIFFERENCE-EQ SET-DIFFERENCE-EQUAL
        SET-DIFFERENCE-THEORIES
        SET-DUPLICATE-KEYS-ACTION
        SET-DUPLICATE-KEYS-ACTION!
        SET-ENFORCE-REDUNDANCY
        SET-EQUALP-EQUAL SET-EVISC-TUPLE
        SET-FC-CRITERIA SET-FC-REPORT-ON-THE-FLY
        SET-FMT-HARD-RIGHT-MARGIN
        SET-FMT-SOFT-RIGHT-MARGIN
        SET-GAG-MODE SET-GC-STRATEGY SET-GUARD-CHECKING SET-GUARD-MSG
        SET-IGNORE-OK SET-INHIBIT-OUTPUT-LST
        SET-INHIBIT-WARNINGS SET-INHIBIT-WARNINGS!
        SET-INHIBITED-SUMMARY-TYPES
        SET-INVISIBLE-FNS-TABLE
        SET-IPRINT SET-IRRELEVANT-FORMALS-OK
        SET-LD-KEYWORD-ALIASES SET-LD-KEYWORD-ALIASES!
        SET-LD-PROMPT SET-LD-REDEFINITION-ACTION
        SET-LD-SKIP-PROOFS
        SET-LD-SKIP-PROOFSP SET-LET*-ABSTRACTION
        SET-LET*-ABSTRACTIONP
        SET-MATCH-FREE-DEFAULT
        SET-MATCH-FREE-ERROR
        SET-MEASURE-FUNCTION SET-NON-LINEAR
        SET-NON-LINEARP
        SET-OVERRIDE-HINTS SET-OVERRIDE-HINTS!
        SET-PARALLEL-EXECUTION
        SET-PRINT-BASE SET-PRINT-BASE-RADIX SET-PRINT-CASE
        SET-PRINT-CIRCLE SET-PRINT-CLAUSE-IDS
        SET-PRINT-ESCAPE SET-PRINT-GV-DEFAULTS SET-PRINT-LENGTH
        SET-PRINT-LEVEL SET-PRINT-LINES
        SET-PRINT-RADIX SET-PRINT-READABLY
        SET-PRINT-RIGHT-MARGIN SET-PROVER-STEP-LIMIT SET-RAW-MODE
        SET-RAW-MODE-ON SET-RAW-MODE-ON!
        SET-RAW-PROOF-FORMAT SET-RAW-WARNING-FORMAT
        SET-REGISTER-INVARIANT-RISK SET-REWRITE-STACK-LIMIT
        SET-RULER-EXTENDERS
        SET-RW-CACHE-STATE SET-RW-CACHE-STATE!
        SET-SAVED-OUTPUT SET-SERIALIZE-CHARACTER SET-SERIALIZE-CHARACTER-SYSTEM
        SET-SKIP-META-TERMP-CHECKS SET-SKIP-META-TERMP-CHECKS!
        SET-SLOW-ALIST-ACTION SET-SPLITTER-OUTPUT SET-STATE-OK
        SET-TAU-AUTO-MODE
        SET-TEMP-TOUCHABLE-VARS SET-TEMP-TOUCHABLE-FNS
        SET-TIMER
        SET-TOTAL-PARALLELISM-WORK-LIMIT
        SET-TOTAL-PARALLELISM-WORK-LIMIT-ERROR
        SET-TRACE-EVISC-TUPLE SET-VERIFY-GUARDS-EAGERNESS
        SET-W
        SET-WATERFALL-PARALLELISM
        SET-WATERFALL-PARALLELISM-HACKS-ENABLED
        SET-WATERFALL-PARALLELISM-HACKS-ENABLED!
        SET-WATERFALL-PRINTING
        SET-WELL-FOUNDED-RELATION
        SET-WORMHOLE-DATA
        SET-WORMHOLE-ENTRY-CODE SET-WRITE-ACL2X SETENV$ SEVENTH
        SGETPROP SHOW-ACCUMULATED-PERSISTENCE
        SHOW-BDD SHOW-BODIES SHOW-CUSTOM-KEYWORD-HINT-EXPANSION
        SHOW-FC-CRITERIA SHRINK-32-BIT-INTEGER-STACK
        SHRINK-T-STACK
        SIGNED-BYTE SIGNED-BYTE-P SIGNUM SIMPLIFY
        SIXTH SKIP-PROOFS SLEEP SOME-SLASHABLE SPEC-MV-LET
        SPLITTER-OUTPUT STABLE-UNDER-SIMPLIFICATIONP
        STANDARD-CHAR STANDARD-CHAR-LISTP
        STANDARD-CHAR-LISTP-APPEND
        STANDARD-CHAR-LISTP-FORWARD-TO-CHARACTER-LISTP
        STANDARD-CHAR-P
        STANDARD-CHAR-P-NTH STANDARD-CO
        STANDARD-OI STANDARD-STRING-ALISTP
        STANDARD-STRING-ALISTP-FORWARD-TO-ALISTP
        START-PROOF-TREE
        STATE STATE-GLOBAL-LET* STATE-GLOBAL-LET*-CLEANUP
        STATE-GLOBAL-LET*-GET-GLOBALS
        STATE-GLOBAL-LET*-PUT-GLOBALS STATE-P
        STATE-P-IMPLIES-AND-FORWARD-TO-STATE-P1
        STATE-P1 STATE-P1-FORWARD
        STATE-P1-UPDATE-MAIN-TIMER
        STATE-P1-UPDATE-NTH-2-WORLD
        STEP-LIMIT STOBJ-LET STOP-PROOF-TREE
        STRING STRING-APPEND STRING-APPEND-LST
        STRING-DOWNCASE STRING-DOWNCASE1
        STRING-EQUAL STRING-EQUAL1
        STRING-IS-NOT-CIRCULAR STRING-LISTP
        STRING-UPCASE STRING-UPCASE1
        STRING< STRING<-IRREFLEXIVE
        STRING<-L STRING<-L-ASYMMETRIC
        STRING<-L-IRREFLEXIVE
        STRING<-L-TRANSITIVE
        STRING<-L-TRICHOTOMY
        STRING<= STRING> STRING>=
        STRINGP STRINGP-SYMBOL-PACKAGE-NAME
        STRIP-CARS STRIP-CDRS
        SUBLIS SUBLIS-FN SUBLIS-FN-LST-SIMPLE SUBLIS-FN-SIMPLE
        SUBSEQ SUBSEQ-LIST SUBSETP SUBSETP-EQ SUBSETP-EQUAL
        SUBST SUBSTITUTE SUBSTITUTE-AC SUMMARY
        SYMBOL SYMBOL-< SYMBOL-<-ASYMMETRIC
        SYMBOL-<-IRREFLEXIVE SYMBOL-<-TRANSITIVE
        SYMBOL-<-TRICHOTOMY SYMBOL-ALISTP
        SYMBOL-ALISTP-FORWARD-TO-EQLABLE-ALISTP
        SYMBOL-DOUBLET-LISTP
        SYMBOL-EQUALITY SYMBOL-LISTP
        SYMBOL-LISTP-FORWARD-TO-TRUE-LISTP
        SYMBOL-NAME
        SYMBOL-NAME-INTERN-IN-PACKAGE-OF-SYMBOL
        SYMBOL-PACKAGE-NAME SYMBOLP
        SYMBOLP-INTERN-IN-PACKAGE-OF-SYMBOL
        SYNP SYNTAXP SYS-CALL SYS-CALL* SYS-CALL+ SYS-CALL-STATUS
        T T-STACK T-STACK-LENGTH T-STACK-LENGTH1
        TABLE TABLE-ALIST TAKE
        TAU-DATA TAU-DATABASE
        TAU-INTERVAL-DOM
        TAU-INTERVAL-HI TAU-INTERVAL-HI-REL
        TAU-INTERVAL-LO TAU-INTERVAL-LO-REL
        TAU-INTERVALP
        TAU-STATUS TAU-SYSTEM
        TENTH TERM-LIST-LISTP TERM-LISTP TERM-ORDER TERMINATION-THEOREM TERMP
        THE THE-CHECK THE-FIXNUM
        THE-FIXNUM! THEORY THEORY-INVARIANT
        THIRD THM TIME$ TIME-TRACKER TIME-TRACKER-TAU TIMER-ALISTP
        TIMER-ALISTP-FORWARD-TO-TRUE-LIST-LISTP-AND-SYMBOL-ALISTP
        TOGGLE-PC-MACRO
        TOP-LEVEL TRACE! TRACE$ TRANS
        TRANS! TRANS1 TRANSLATE-AND-TEST TRICHOTOMY TRUE-LIST-LISTP
        TRUE-LIST-LISTP-FORWARD-TO-TRUE-LISTP
        TRUE-LIST-LISTP-FORWARD-TO-TRUE-LISTP-ASSOC-EQUAL
        TRUE-LISTP
        TRUE-LISTP-CADR-ASSOC-EQ-FOR-OPEN-CHANNELS-P
        TRUE-LISTP-UPDATE-NTH
        TRUNCATE TTAG TTAGS-SEEN TTHM TYPE
        TYPED-IO-LISTP TYPED-IO-LISTP-FORWARD-TO-TRUE-LISTP
        TYPESPEC-CHECK
        U UBT UBT!
        UBT-PREHISTORY UBT? UBU UBU! UBU? UNARY-- UNARY-/
        UNARY-FUNCTION-SYMBOL-LISTP UNICITY-OF-0
        UNICITY-OF-1 UNION$ UNION-EQ UNION-EQUAL
        UNION-THEORIES UNIVERSAL-THEORY
        UNMONITOR UNQUOTE UNSAVE UNSIGNED-BYTE UNSIGNED-BYTE-P
        UNTRACE$ UNTRANS-TABLE
        UNTRANSLATE UPDATE-32-BIT-INTEGER-STACK
        UPDATE-ACL2-ORACLE
        UPDATE-ACL2-ORACLE-PRESERVES-STATE-P1
        UPDATE-BIG-CLOCK-ENTRY UPDATE-FILE-CLOCK
        UPDATE-GLOBAL-TABLE UPDATE-IDATES
        UPDATE-LIST-ALL-PACKAGE-NAMES-LST
        UPDATE-NTH UPDATE-NTH-ARRAY
        UPDATE-OPEN-INPUT-CHANNELS UPDATE-OPEN-OUTPUT-CHANNELS
        UPDATE-READ-FILES
        UPDATE-T-STACK UPDATE-USER-STOBJ-ALIST
        UPDATE-USER-STOBJ-ALIST1
        UPDATE-WRITTEN-FILES
        UPPER-CASE-P UPPER-CASE-P-CHAR-UPCASE
        UPPER-CASE-P-FORWARD-TO-ALPHA-CHAR-P
        USER-STOBJ-ALIST USER-STOBJ-ALIST1
        VALUE VALUE-TRIPLE VERBOSE-PSTACK VERIFY
        VERIFY-GUARDS VERIFY-GUARDS+ VERIFY-GUARDS-FORMULA
        VERIFY-TERMINATION W WALKABOUT
        WARNING! WATERFALL-PARALLELISM WATERFALL-PRINTING
        WET WITH-FAST-ALIST
        WITH-GUARD-CHECKING WITH-GUARD-CHECKING-ERROR-TRIPLE
        WITH-GUARD-CHECKING-EVENT
        WITH-LIVE-STATE WITH-LOCAL-STATE WITH-LOCAL-STOBJ
        WITH-OUTPUT WITH-OUTPUT! WITH-OUTPUT-LOCK
        WITH-PROVER-STEP-LIMIT WITH-PROVER-STEP-LIMIT!
        WITH-PROVER-TIME-LIMIT WITH-SERIALIZE-CHARACTER
        WITH-STOLEN-ALIST WITHOUT-EVISC
        WOF WORLD WORMHOLE WORMHOLE-DATA
        WORMHOLE-ENTRY-CODE WORMHOLE-EVAL
        WORMHOLE-P WORMHOLE-STATUSP
        WORMHOLE1 WRITABLE-FILE-LISTP
        WRITABLE-FILE-LISTP-FORWARD-TO-TRUE-LIST-LISTP
        WRITABLE-FILE-LISTP1
        WRITABLE-FILE-LISTP1-FORWARD-TO-TRUE-LISTP-AND-CONSP
        WRITE-BYTE$
        WRITEABLE-FILES WRITEABLE-FILES-P
        WRITEABLE-FILES-P-FORWARD-TO-WRITABLE-FILE-LISTP
        WRITTEN-FILE
        WRITTEN-FILE-FORWARD-TO-TRUE-LISTP-AND-CONSP
        WRITTEN-FILE-LISTP
        WRITTEN-FILE-LISTP-FORWARD-TO-TRUE-LIST-LISTP-AND-ALISTP
        WRITTEN-FILES WRITTEN-FILES-P
        WRITTEN-FILES-P-FORWARD-TO-WRITTEN-FILE-LISTP
        XARGS XOR XXXJOIN ZERO ZEROP ZIP ZP ZPF

; For ACL2(r):

        DEFTHM-STD DEFUN-STD DEFUNS-STD
        I-CLOSE I-LARGE I-LIMITED I-SMALL
        REAL-LISTP STANDARD-PART STANDARDP)))

  "This is the list of ACL2 symbols that the ordinary user is extremely
likely to want to include in the import list of any package created
because these symbols are the basic hooks for using ACL2.  However,
it is never necessary to do such importing: one can always use the
acl2:: prefix."

  )

(defpkg "ACL2-USER"
  (union-eq *acl2-exports*
            *common-lisp-symbols-from-main-lisp-package*))