tests/inputs/PKGS.sml

384     ("GET-INTERNAL-RUN-TIME" , "ACL2" , "COMMON-LISP"),
1708     ("GET-INTERNAL-RUN-TIME" , "ACL2-USER" , "COMMON-LISP"),
2077     ("NTH-0-READ-RUN-TIME-TYPE-PRESCRIPTION" , "ACL2-USER" , "ACL2"),
2308     ("READ-RUN-TIME" , "ACL2-USER" , "ACL2"),
2309     ("READ-RUN-TIME-PRESERVES-STATE-P1" , "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"),
3620     ("GET-INTERNAL-RUN-TIME" , "U" , "COMMON-LISP"),
3989     ("NTH-0-READ-RUN-TIME-TYPE-PRESCRIPTION" , "U" , "ACL2"),
4216     ("READ-RUN-TIME" , "U" , "ACL2"),
4217     ("READ-RUN-TIME-PRESERVES-STATE-P1" , "U" , "ACL2"),
5457     ("GET-INTERNAL-RUN-TIME" , "ACL2-ASG" , "COMMON-LISP"),
5826     ("NTH-0-READ-RUN-TIME-TYPE-PRESCRIPTION" , "ACL2-ASG" , "ACL2"),
6057     ("READ-RUN-TIME" , "ACL2-ASG" , "ACL2"),
6058     ("READ-RUN-TIME-PRESERVES-STATE-P1" , "ACL2-ASG" , "ACL2"),
7306     ("GET-INTERNAL-RUN-TIME" , "ACL2-AGP" , "COMMON-LISP"),
7675     ("NTH-0-READ-RUN-TIME-TYPE-PRESCRIPTION" , "ACL2-AGP" , "ACL2"),
7906     ("READ-RUN-TIME" , "ACL2-AGP" , "ACL2"),
7907     ("READ-RUN-TIME-PRESERVES-STATE-P1" , "ACL2-AGP" , "ACL2"),
9155     ("GET-INTERNAL-RUN-TIME" , "ACL2-CRG" , "COMMON-LISP"),
9524     ("NTH-0-READ-RUN-TIME-TYPE-PRESCRIPTION" , "ACL2-CRG" , "ACL2"),
9755     ("READ-RUN-TIME" , "ACL2-CRG" , "ACL2"),
9756     ("READ-RUN-TIME-PRESERVES-STATE-P1" , "ACL2-CRG" , "ACL2"),
10284     "M1",