tests/inputs/PKGS.sml

655     ("NTH" , "ACL2" , "COMMON-LISP"),
657     ("NTH-VALUE" , "ACL2" , "COMMON-LISP"),
963     ("UPDATE-INSTANCE-FOR-DIFFERENT-CLASS" , "ACL2" , "COMMON-LISP"),
965     ("UPDATE-INSTANCE-FOR-REDEFINED-CLASS" , "ACL2" , "COMMON-LISP"),
1092     ("ADD-NTH-ALIAS" , "ACL2-USER" , "ACL2"),
1334     ("CHARACTERP-NTH" , "ACL2-USER" , "ACL2"),
1875     ("LEN-UPDATE-NTH" , "ACL2-USER" , "ACL2"),
2035     ("MV-NTH" , "ACL2-USER" , "ACL2"),
2075     ("NTH" , "ACL2-USER" , "COMMON-LISP"),
2076     ("NTH-0-CONS" , "ACL2-USER" , "ACL2"),
2077     ("NTH-0-READ-RUN-TIME-TYPE-PRESCRIPTION" , "ACL2-USER" , "ACL2"),
2078     ("NTH-ADD1" , "ACL2-USER" , "ACL2"),
2079     ("NTH-ALIASES" , "ACL2-USER" , "ACL2"),
2080     ("NTH-UPDATE-NTH" , "ACL2-USER" , "ACL2"),
2081     ("NTH-VALUE" , "ACL2-USER" , "COMMON-LISP"),
2356     ("REMOVE-NTH-ALIAS" , "ACL2-USER" , "ACL2"),
2527     ("STANDARD-CHAR-P-NTH" , "ACL2-USER" , "ACL2"),
2545     ("STATE-P1-UPDATE-MAIN-TIMER" , "ACL2-USER" , "ACL2"),
2546     ("STATE-P1-UPDATE-NTH-2-WORLD" , "ACL2-USER" , "ACL2"),
2687     ("TRUE-LISTP-UPDATE-NTH" , "ACL2-USER" , "ACL2"),
2731     ("UPDATE-32-BIT-INTEGER-STACK" , "ACL2-USER" , "ACL2"),
2732     ("UPDATE-ACL2-ORACLE" , "ACL2-USER" , "ACL2"),
2733     ("UPDATE-ACL2-ORACLE-PRESERVES-STATE-P1" , "ACL2-USER" , "ACL2"),
2734     ("UPDATE-BIG-CLOCK-ENTRY" , "ACL2-USER" , "ACL2"),
2735     ("UPDATE-FILE-CLOCK" , "ACL2-USER" , "ACL2"),
2736     ("UPDATE-GLOBAL-TABLE" , "ACL2-USER" , "ACL2"),
2737     ("UPDATE-IDATES" , "ACL2-USER" , "ACL2"),
2738     ("UPDATE-INSTANCE-FOR-DIFFERENT-CLASS" , "ACL2-USER" , "COMMON-LISP"),
2739     ("UPDATE-INSTANCE-FOR-REDEFINED-CLASS" , "ACL2-USER" , "COMMON-LISP"),
2740     ("UPDATE-LIST-ALL-PACKAGE-NAMES-LST" , "ACL2-USER" , "ACL2"),
2741     ("UPDATE-NTH" , "ACL2-USER" , "ACL2"),
2742     ("UPDATE-OPEN-INPUT-CHANNELS" , "ACL2-USER" , "ACL2"),
2743     ("UPDATE-OPEN-OUTPUT-CHANNELS" , "ACL2-USER" , "ACL2"),
2744     ("UPDATE-READ-FILES" , "ACL2-USER" , "ACL2"),
2745     ("UPDATE-T-STACK" , "ACL2-USER" , "ACL2"),
2746     ("UPDATE-USER-STOBJ-ALIST" , "ACL2-USER" , "ACL2"),
2747     ("UPDATE-USER-STOBJ-ALIST1" , "ACL2-USER" , "ACL2"),
2748     ("UPDATE-WRITTEN-FILES" , "ACL2-USER" , "ACL2"),
2833     ("&REST" , "M1" , "COMMON-LISP"),
2834     ("*" , "M1" , "COMMON-LISP"),
2835     ("+" , "M1" , "COMMON-LISP"),
2836     ("-" , "M1" , "COMMON-LISP"),
2837     ("/" , "M1" , "COMMON-LISP"),
2838     ("<" , "M1" , "COMMON-LISP"),
2839     ("<=" , "M1" , "COMMON-LISP"),
2840     (">" , "M1" , "COMMON-LISP"),
2841     (">=" , "M1" , "COMMON-LISP"),
2842     ("ACL2-COUNT" , "M1" , "ACL2"),
2843     ("AND" , "M1" , "COMMON-LISP"),
2844     ("ASSOC" , "M1" , "COMMON-LISP"),
2845     ("ATOM" , "M1" , "COMMON-LISP"),
2846     ("CAR" , "M1" , "COMMON-LISP"),
2847     ("CASE" , "M1" , "COMMON-LISP"),
2848     ("CDR" , "M1" , "COMMON-LISP"),
2849     ("COERCE" , "M1" , "COMMON-LISP"),
2850     ("CONCATENATE" , "M1" , "COMMON-LISP"),
2851     ("COND" , "M1" , "COMMON-LISP"),
2852     ("CONS" , "M1" , "COMMON-LISP"),
2853     ("CONSP" , "M1" , "COMMON-LISP"),
2854     ("DECLARE" , "M1" , "COMMON-LISP"),
2855     ("DEFCONST" , "M1" , "ACL2"),
2856     ("DEFMACRO" , "M1" , "COMMON-LISP"),
2857     ("DEFTHM" , "M1" , "ACL2"),
2858     ("DEFUN" , "M1" , "COMMON-LISP"),
2859     ("DISABLE" , "M1" , "ACL2"),
2860     ("E/D" , "M1" , "ACL2"),
2861     ("ENDP" , "M1" , "COMMON-LISP"),
2862     ("EQUAL" , "M1" , "COMMON-LISP"),
2863     ("EXPT" , "M1" , "COMMON-LISP"),
2864     ("IF" , "M1" , "COMMON-LISP"),
2865     ("IGNORE" , "M1" , "COMMON-LISP"),
2866     ("IMPLIES" , "M1" , "ACL2"),
2867     ("IN-THEORY" , "M1" , "ACL2"),
2868     ("INCLUDE-BOOK" , "M1" , "ACL2"),
2869     ("INTERN-IN-PACKAGE-OF-SYMBOL" , "M1" , "ACL2"),
2870     ("LET" , "M1" , "COMMON-LISP"),
2871     ("LET*" , "M1" , "COMMON-LISP"),
2872     ("LIST" , "M1" , "COMMON-LISP"),
2873     ("LIST*" , "M1" , "COMMON-LISP"),
2874     ("MOD" , "M1" , "COMMON-LISP"),
2875     ("MUTUAL-RECURSION" , "M1" , "ACL2"),
2876     ("NATP" , "M1" , "ACL2"),
2877     ("NIL" , "M1" , "COMMON-LISP"),
2878     ("NOT" , "M1" , "COMMON-LISP"),
2879     ("O-P" , "M1" , "ACL2"),
2880     ("O<" , "M1" , "ACL2"),
2881     ("OR" , "M1" , "COMMON-LISP"),
2882     ("OTHERWISE" , "M1" , "COMMON-LISP"),
2883     ("PAIRLIS$" , "M1" , "ACL2"),
2884     ("PAIRLIS-X2" , "M1" , "ACL2"),
2885     ("PROGN" , "M1" , "COMMON-LISP"),
2886     ("QUOTE" , "M1" , "COMMON-LISP"),
2887     ("QUOTEP" , "M1" , "ACL2"),
2888     ("STRING" , "M1" , "COMMON-LISP"),
2889     ("STRIP-CARS" , "M1" , "ACL2"),
2890     ("SYMBOL-NAME" , "M1" , "COMMON-LISP"),
2891     ("SYMBOLP" , "M1" , "COMMON-LISP"),
2892     ("SYNTAXP" , "M1" , "ACL2"),
2893     ("T" , "M1" , "COMMON-LISP"),
2894     ("XARGS" , "M1" , "ACL2"),
2895     ("ZP" , "M1" , "ACL2"),
3005     ("ADD-NTH-ALIAS" , "U" , "ACL2"),
3246     ("CHARACTERP-NTH" , "U" , "ACL2"),
3787     ("LEN-UPDATE-NTH" , "U" , "ACL2"),
3947     ("MV-NTH" , "U" , "ACL2"),
3987     ("NTH" , "U" , "COMMON-LISP"),
3988     ("NTH-0-CONS" , "U" , "ACL2"),
3989     ("NTH-0-READ-RUN-TIME-TYPE-PRESCRIPTION" , "U" , "ACL2"),
3990     ("NTH-ADD1" , "U" , "ACL2"),
3991     ("NTH-ALIASES" , "U" , "ACL2"),
3992     ("NTH-UPDATE-NTH" , "U" , "ACL2"),
3993     ("NTH-VALUE" , "U" , "COMMON-LISP"),
4262     ("REMOVE-NTH-ALIAS" , "U" , "ACL2"),
4432     ("STANDARD-CHAR-P-NTH" , "U" , "ACL2"),
4450     ("STATE-P1-UPDATE-MAIN-TIMER" , "U" , "ACL2"),
4451     ("STATE-P1-UPDATE-NTH-2-WORLD" , "U" , "ACL2"),
4590     ("TRUE-LISTP-UPDATE-NTH" , "U" , "ACL2"),
4634     ("UPDATE-32-BIT-INTEGER-STACK" , "U" , "ACL2"),
4635     ("UPDATE-ACL2-ORACLE" , "U" , "ACL2"),
4636     ("UPDATE-ACL2-ORACLE-PRESERVES-STATE-P1" , "U" , "ACL2"),
4637     ("UPDATE-BIG-CLOCK-ENTRY" , "U" , "ACL2"),
4638     ("UPDATE-FILE-CLOCK" , "U" , "ACL2"),
4639     ("UPDATE-GLOBAL-TABLE" , "U" , "ACL2"),
4640     ("UPDATE-IDATES" , "U" , "ACL2"),
4641     ("UPDATE-INSTANCE-FOR-DIFFERENT-CLASS" , "U" , "COMMON-LISP"),
4642     ("UPDATE-INSTANCE-FOR-REDEFINED-CLASS" , "U" , "COMMON-LISP"),
4643     ("UPDATE-LIST-ALL-PACKAGE-NAMES-LST" , "U" , "ACL2"),
4644     ("UPDATE-NTH" , "U" , "ACL2"),
4645     ("UPDATE-OPEN-INPUT-CHANNELS" , "U" , "ACL2"),
4646     ("UPDATE-OPEN-OUTPUT-CHANNELS" , "U" , "ACL2"),
4647     ("UPDATE-READ-FILES" , "U" , "ACL2"),
4648     ("UPDATE-T-STACK" , "U" , "ACL2"),
4649     ("UPDATE-USER-STOBJ-ALIST" , "U" , "ACL2"),
4650     ("UPDATE-USER-STOBJ-ALIST1" , "U" , "ACL2"),
4651     ("UPDATE-WRITTEN-FILES" , "U" , "ACL2"),
4841     ("ADD-NTH-ALIAS" , "ACL2-ASG" , "ACL2"),
5083     ("CHARACTERP-NTH" , "ACL2-ASG" , "ACL2"),
5624     ("LEN-UPDATE-NTH" , "ACL2-ASG" , "ACL2"),
5784     ("MV-NTH" , "ACL2-ASG" , "ACL2"),
5824     ("NTH" , "ACL2-ASG" , "COMMON-LISP"),
5825     ("NTH-0-CONS" , "ACL2-ASG" , "ACL2"),
5826     ("NTH-0-READ-RUN-TIME-TYPE-PRESCRIPTION" , "ACL2-ASG" , "ACL2"),
5827     ("NTH-ADD1" , "ACL2-ASG" , "ACL2"),
5828     ("NTH-ALIASES" , "ACL2-ASG" , "ACL2"),
5829     ("NTH-UPDATE-NTH" , "ACL2-ASG" , "ACL2"),
5830     ("NTH-VALUE" , "ACL2-ASG" , "COMMON-LISP"),
6105     ("REMOVE-NTH-ALIAS" , "ACL2-ASG" , "ACL2"),
6276     ("STANDARD-CHAR-P-NTH" , "ACL2-ASG" , "ACL2"),
6294     ("STATE-P1-UPDATE-MAIN-TIMER" , "ACL2-ASG" , "ACL2"),
6295     ("STATE-P1-UPDATE-NTH-2-WORLD" , "ACL2-ASG" , "ACL2"),
6436     ("TRUE-LISTP-UPDATE-NTH" , "ACL2-ASG" , "ACL2"),
6480     ("UPDATE-32-BIT-INTEGER-STACK" , "ACL2-ASG" , "ACL2"),
6481     ("UPDATE-ACL2-ORACLE" , "ACL2-ASG" , "ACL2"),
6482     ("UPDATE-ACL2-ORACLE-PRESERVES-STATE-P1" , "ACL2-ASG" , "ACL2"),
6483     ("UPDATE-BIG-CLOCK-ENTRY" , "ACL2-ASG" , "ACL2"),
6484     ("UPDATE-FILE-CLOCK" , "ACL2-ASG" , "ACL2"),
6485     ("UPDATE-GLOBAL-TABLE" , "ACL2-ASG" , "ACL2"),
6486     ("UPDATE-IDATES" , "ACL2-ASG" , "ACL2"),
6487     ("UPDATE-INSTANCE-FOR-DIFFERENT-CLASS" , "ACL2-ASG" , "COMMON-LISP"),
6488     ("UPDATE-INSTANCE-FOR-REDEFINED-CLASS" , "ACL2-ASG" , "COMMON-LISP"),
6489     ("UPDATE-LIST-ALL-PACKAGE-NAMES-LST" , "ACL2-ASG" , "ACL2"),
6490     ("UPDATE-NTH" , "ACL2-ASG" , "ACL2"),
6491     ("UPDATE-OPEN-INPUT-CHANNELS" , "ACL2-ASG" , "ACL2"),
6492     ("UPDATE-OPEN-OUTPUT-CHANNELS" , "ACL2-ASG" , "ACL2"),
6493     ("UPDATE-READ-FILES" , "ACL2-ASG" , "ACL2"),
6494     ("UPDATE-T-STACK" , "ACL2-ASG" , "ACL2"),
6495     ("UPDATE-USER-STOBJ-ALIST" , "ACL2-ASG" , "ACL2"),
6496     ("UPDATE-USER-STOBJ-ALIST1" , "ACL2-ASG" , "ACL2"),
6497     ("UPDATE-WRITTEN-FILES" , "ACL2-ASG" , "ACL2"),
6690     ("ADD-NTH-ALIAS" , "ACL2-AGP" , "ACL2"),
6932     ("CHARACTERP-NTH" , "ACL2-AGP" , "ACL2"),
7473     ("LEN-UPDATE-NTH" , "ACL2-AGP" , "ACL2"),
7633     ("MV-NTH" , "ACL2-AGP" , "ACL2"),
7673     ("NTH" , "ACL2-AGP" , "COMMON-LISP"),
7674     ("NTH-0-CONS" , "ACL2-AGP" , "ACL2"),
7675     ("NTH-0-READ-RUN-TIME-TYPE-PRESCRIPTION" , "ACL2-AGP" , "ACL2"),
7676     ("NTH-ADD1" , "ACL2-AGP" , "ACL2"),
7677     ("NTH-ALIASES" , "ACL2-AGP" , "ACL2"),
7678     ("NTH-UPDATE-NTH" , "ACL2-AGP" , "ACL2"),
7679     ("NTH-VALUE" , "ACL2-AGP" , "COMMON-LISP"),
7954     ("REMOVE-NTH-ALIAS" , "ACL2-AGP" , "ACL2"),
8125     ("STANDARD-CHAR-P-NTH" , "ACL2-AGP" , "ACL2"),
8143     ("STATE-P1-UPDATE-MAIN-TIMER" , "ACL2-AGP" , "ACL2"),
8144     ("STATE-P1-UPDATE-NTH-2-WORLD" , "ACL2-AGP" , "ACL2"),
8285     ("TRUE-LISTP-UPDATE-NTH" , "ACL2-AGP" , "ACL2"),
8329     ("UPDATE-32-BIT-INTEGER-STACK" , "ACL2-AGP" , "ACL2"),
8330     ("UPDATE-ACL2-ORACLE" , "ACL2-AGP" , "ACL2"),
8331     ("UPDATE-ACL2-ORACLE-PRESERVES-STATE-P1" , "ACL2-AGP" , "ACL2"),
8332     ("UPDATE-BIG-CLOCK-ENTRY" , "ACL2-AGP" , "ACL2"),
8333     ("UPDATE-FILE-CLOCK" , "ACL2-AGP" , "ACL2"),
8334     ("UPDATE-GLOBAL-TABLE" , "ACL2-AGP" , "ACL2"),
8335     ("UPDATE-IDATES" , "ACL2-AGP" , "ACL2"),
8336     ("UPDATE-INSTANCE-FOR-DIFFERENT-CLASS" , "ACL2-AGP" , "COMMON-LISP"),
8337     ("UPDATE-INSTANCE-FOR-REDEFINED-CLASS" , "ACL2-AGP" , "COMMON-LISP"),
8338     ("UPDATE-LIST-ALL-PACKAGE-NAMES-LST" , "ACL2-AGP" , "ACL2"),
8339     ("UPDATE-NTH" , "ACL2-AGP" , "ACL2"),
8340     ("UPDATE-OPEN-INPUT-CHANNELS" , "ACL2-AGP" , "ACL2"),
8341     ("UPDATE-OPEN-OUTPUT-CHANNELS" , "ACL2-AGP" , "ACL2"),
8342     ("UPDATE-READ-FILES" , "ACL2-AGP" , "ACL2"),
8343     ("UPDATE-T-STACK" , "ACL2-AGP" , "ACL2"),
8344     ("UPDATE-USER-STOBJ-ALIST" , "ACL2-AGP" , "ACL2"),
8345     ("UPDATE-USER-STOBJ-ALIST1" , "ACL2-AGP" , "ACL2"),
8346     ("UPDATE-WRITTEN-FILES" , "ACL2-AGP" , "ACL2"),
8539     ("ADD-NTH-ALIAS" , "ACL2-CRG" , "ACL2"),
8781     ("CHARACTERP-NTH" , "ACL2-CRG" , "ACL2"),
9322     ("LEN-UPDATE-NTH" , "ACL2-CRG" , "ACL2"),
9482     ("MV-NTH" , "ACL2-CRG" , "ACL2"),
9522     ("NTH" , "ACL2-CRG" , "COMMON-LISP"),
9523     ("NTH-0-CONS" , "ACL2-CRG" , "ACL2"),
9524     ("NTH-0-READ-RUN-TIME-TYPE-PRESCRIPTION" , "ACL2-CRG" , "ACL2"),
9525     ("NTH-ADD1" , "ACL2-CRG" , "ACL2"),
9526     ("NTH-ALIASES" , "ACL2-CRG" , "ACL2"),
9527     ("NTH-UPDATE-NTH" , "ACL2-CRG" , "ACL2"),
9528     ("NTH-VALUE" , "ACL2-CRG" , "COMMON-LISP"),
9803     ("REMOVE-NTH-ALIAS" , "ACL2-CRG" , "ACL2"),
9974     ("STANDARD-CHAR-P-NTH" , "ACL2-CRG" , "ACL2"),
9992     ("STATE-P1-UPDATE-MAIN-TIMER" , "ACL2-CRG" , "ACL2"),
9993     ("STATE-P1-UPDATE-NTH-2-WORLD" , "ACL2-CRG" , "ACL2"),
10134     ("TRUE-LISTP-UPDATE-NTH" , "ACL2-CRG" , "ACL2"),
10178     ("UPDATE-32-BIT-INTEGER-STACK" , "ACL2-CRG" , "ACL2"),
10179     ("UPDATE-ACL2-ORACLE" , "ACL2-CRG" , "ACL2"),
10180     ("UPDATE-ACL2-ORACLE-PRESERVES-STATE-P1" , "ACL2-CRG" , "ACL2"),
10181     ("UPDATE-BIG-CLOCK-ENTRY" , "ACL2-CRG" , "ACL2"),
10182     ("UPDATE-FILE-CLOCK" , "ACL2-CRG" , "ACL2"),
10183     ("UPDATE-GLOBAL-TABLE" , "ACL2-CRG" , "ACL2"),
10184     ("UPDATE-IDATES" , "ACL2-CRG" , "ACL2"),
10185     ("UPDATE-INSTANCE-FOR-DIFFERENT-CLASS" , "ACL2-CRG" , "COMMON-LISP"),
10186     ("UPDATE-INSTANCE-FOR-REDEFINED-CLASS" , "ACL2-CRG" , "COMMON-LISP"),
10187     ("UPDATE-LIST-ALL-PACKAGE-NAMES-LST" , "ACL2-CRG" , "ACL2"),
10188     ("UPDATE-NTH" , "ACL2-CRG" , "ACL2"),
10189     ("UPDATE-OPEN-INPUT-CHANNELS" , "ACL2-CRG" , "ACL2"),
10190     ("UPDATE-OPEN-OUTPUT-CHANNELS" , "ACL2-CRG" , "ACL2"),
10191     ("UPDATE-READ-FILES" , "ACL2-CRG" , "ACL2"),
10192     ("UPDATE-T-STACK" , "ACL2-CRG" , "ACL2"),
10193     ("UPDATE-USER-STOBJ-ALIST" , "ACL2-CRG" , "ACL2"),
10194     ("UPDATE-USER-STOBJ-ALIST1" , "ACL2-CRG" , "ACL2"),
10195     ("UPDATE-WRITTEN-FILES" , "ACL2-CRG" , "ACL2"),
10284     "M1",