round-trip/gold/axioms.lisp

0 (IN-PACKAGE "ACL2")
1036 (DEFAXIOM SYMBOLP-INTERN-IN-PACKAGE-OF-SYMBOL
1037           (SYMBOLP (INTERN-IN-PACKAGE-OF-SYMBOL X Y)))
1053 (DEFAXIOM INTERN-IN-PACKAGE-OF-SYMBOL-SYMBOL-NAME
1058                    (EQUAL (INTERN-IN-PACKAGE-OF-SYMBOL (SYMBOL-NAME X)
1096      SYMBOL-NAME-INTERN-IN-PACKAGE-OF-SYMBOL
1100               (EQUAL (SYMBOL-NAME (INTERN-IN-PACKAGE-OF-SYMBOL S ANY-SYMBOL))
1111               (EQUAL (SYMBOL-PACKAGE-NAME (INTERN-IN-PACKAGE-OF-SYMBOL X Y))
1122               (EQUAL (SYMBOL-PACKAGE-NAME (INTERN-IN-PACKAGE-OF-SYMBOL X Y))
1162                                      ALPHA-CHAR-P BIT BUILT-IN-CLASS
1178                                      BOOLE-2 CADDR ARRAY-IN-BOUNDS-P
1276                                      IN-PACKAGE FUNCTION-LAMBDA-EXPRESSION
1502   (EQUAL (SYMBOL-PACKAGE-NAME (INTERN-IN-PACKAGE-OF-SYMBOL X Y))
1513               (EQUAL (SYMBOL-PACKAGE-NAME (INTERN-IN-PACKAGE-OF-SYMBOL X Y))
1519          (INTERN-IN-PACKAGE-OF-SYMBOL
1530               (INTERN-IN-PACKAGE-OF-SYMBOL '0 '0))))
1536   (INTERN-IN-PACKAGE-OF-SYMBOL (COERCE (CONS '#\N (CONS '#\I (CONS '#\L '0)))
3838             (IN-LOCAL-FLG)
3839             (IN-PROVE-FLG)
3840             (IN-VERIFY-FLG)
3948                                   THE-MV TABLE IN-ARITHMETIC-THEORY
3952                                   IN-THEORY WITH-OUTPUT-FORCED
3969                                   LIST* APPEND DEFCONST IN-PACKAGE INTERN
4216             (IN-LOCAL-FLG)
4217             (IN-PROVE-FLG)
4218             (IN-VERIFY-FLG)
4326                                   THE-MV TABLE IN-ARITHMETIC-THEORY
4330                                   IN-THEORY WITH-OUTPUT-FORCED
4347                                   LIST* APPEND DEFCONST IN-PACKAGE INTERN
4592             (IN-LOCAL-FLG)
4593             (IN-PROVE-FLG)
4594             (IN-VERIFY-FLG)
4702                                   THE-MV TABLE IN-ARITHMETIC-THEORY
4706                                   IN-THEORY WITH-OUTPUT-FORCED
4723                                   LIST* APPEND DEFCONST IN-PACKAGE INTERN
4975      (IN-LOCAL-FLG)
4976      (IN-PROVE-FLG)
4977      (IN-VERIFY-FLG)
5085                            THE-MV TABLE IN-ARITHMETIC-THEORY
5089                            IN-THEORY WITH-OUTPUT-FORCED
5106                            LIST* APPEND DEFCONST IN-PACKAGE INTERN
5277      (IN-LOCAL-FLG)
5278      (IN-PROVE-FLG)
5279      (IN-VERIFY-FLG)
5387                            THE-MV TABLE IN-ARITHMETIC-THEORY
5391                            IN-THEORY WITH-OUTPUT-FORCED
5408                            LIST* APPEND DEFCONST IN-PACKAGE INTERN
5937          (CONS (CONS (INTERN-IN-PACKAGE-OF-SYMBOL
6250        (INTERN-IN-PACKAGE-OF-SYMBOL
6257        (INTERN-IN-PACKAGE-OF-SYMBOL
7169     (INTERN-IN-PACKAGE-OF-SYMBOL
7680 (DEFAXIOM COMPLETION-OF-INTERN-IN-PACKAGE-OF-SYMBOL
7681           (EQUAL (INTERN-IN-PACKAGE-OF-SYMBOL X Y)
7683                      (INTERN-IN-PACKAGE-OF-SYMBOL X Y)
7829  (INTERN-IN-PACKAGE-OF-SYMBOL