tests/inputs/PKGS.sml

285     ("DEFUN" , "ACL2" , "COMMON-LISP"),
545     ("MAKE-ARRAY" , "ACL2" , "COMMON-LISP"),
547     ("MAKE-BROADCAST-STREAM" , "ACL2" , "COMMON-LISP"),
549     ("MAKE-CONCATENATED-STREAM" , "ACL2" , "COMMON-LISP"),
551     ("MAKE-CONDITION" , "ACL2" , "COMMON-LISP"),
553     ("MAKE-DISPATCH-MACRO-CHARACTER" , "ACL2" , "COMMON-LISP"),
555     ("MAKE-ECHO-STREAM" , "ACL2" , "COMMON-LISP"),
557     ("MAKE-HASH-TABLE" , "ACL2" , "COMMON-LISP"),
559     ("MAKE-INSTANCE" , "ACL2" , "COMMON-LISP"),
561     ("MAKE-INSTANCES-OBSOLETE" , "ACL2" , "COMMON-LISP"),
563     ("MAKE-LIST" , "ACL2" , "COMMON-LISP"),
565     ("MAKE-LOAD-FORM" , "ACL2" , "COMMON-LISP"),
567     ("MAKE-LOAD-FORM-SAVING-SLOTS" , "ACL2" , "COMMON-LISP"),
569     ("MAKE-METHOD" , "ACL2" , "COMMON-LISP"),
571     ("MAKE-PACKAGE" , "ACL2" , "COMMON-LISP"),
573     ("MAKE-PATHNAME" , "ACL2" , "COMMON-LISP"),
575     ("MAKE-RANDOM-STATE" , "ACL2" , "COMMON-LISP"),
577     ("MAKE-SEQUENCE" , "ACL2" , "COMMON-LISP"),
579     ("MAKE-STRING" , "ACL2" , "COMMON-LISP"),
581     ("MAKE-STRING-INPUT-STREAM" , "ACL2" , "COMMON-LISP"),
583     ("MAKE-STRING-OUTPUT-STREAM" , "ACL2" , "COMMON-LISP"),
585     ("MAKE-SYMBOL" , "ACL2" , "COMMON-LISP"),
587     ("MAKE-SYNONYM-STREAM" , "ACL2" , "COMMON-LISP"),
589     ("MAKE-TWO-WAY-STREAM" , "ACL2" , "COMMON-LISP"),
1470     ("DEFAULT-DEFUN-MODE" , "ACL2-USER" , "ACL2"),
1471     ("DEFAULT-DEFUN-MODE-FROM-STATE" , "ACL2-USER" , "ACL2"),
1519     ("DEFUN" , "ACL2-USER" , "COMMON-LISP"),
1520     ("DEFUN-NX" , "ACL2-USER" , "ACL2"),
1521     ("DEFUN-SK" , "ACL2-USER" , "ACL2"),
1935     ("MAKE-ARRAY" , "ACL2-USER" , "COMMON-LISP"),
1936     ("MAKE-BROADCAST-STREAM" , "ACL2-USER" , "COMMON-LISP"),
1937     ("MAKE-CHARACTER-LIST" , "ACL2-USER" , "ACL2"),
1938     ("MAKE-CHARACTER-LIST-MAKE-CHARACTER-LIST" , "ACL2-USER" , "ACL2"),
1939     ("MAKE-CONCATENATED-STREAM" , "ACL2-USER" , "COMMON-LISP"),
1940     ("MAKE-CONDITION" , "ACL2-USER" , "COMMON-LISP"),
1941     ("MAKE-DISPATCH-MACRO-CHARACTER" , "ACL2-USER" , "COMMON-LISP"),
1942     ("MAKE-ECHO-STREAM" , "ACL2-USER" , "COMMON-LISP"),
1943     ("MAKE-EVENT" , "ACL2-USER" , "ACL2"),
1944     ("MAKE-FMT-BINDINGS" , "ACL2-USER" , "ACL2"),
1945     ("MAKE-HASH-TABLE" , "ACL2-USER" , "COMMON-LISP"),
1946     ("MAKE-INPUT-CHANNEL" , "ACL2-USER" , "ACL2"),
1947     ("MAKE-INSTANCE" , "ACL2-USER" , "COMMON-LISP"),
1948     ("MAKE-INSTANCES-OBSOLETE" , "ACL2-USER" , "COMMON-LISP"),
1949     ("MAKE-LIST" , "ACL2-USER" , "COMMON-LISP"),
1950     ("MAKE-LIST-AC" , "ACL2-USER" , "ACL2"),
1951     ("MAKE-LOAD-FORM" , "ACL2-USER" , "COMMON-LISP"),
1952     ("MAKE-LOAD-FORM-SAVING-SLOTS" , "ACL2-USER" , "COMMON-LISP"),
1953     ("MAKE-METHOD" , "ACL2-USER" , "COMMON-LISP"),
1954     ("MAKE-MV-NTHS" , "ACL2-USER" , "ACL2"),
1955     ("MAKE-ORD" , "ACL2-USER" , "ACL2"),
1956     ("MAKE-OUTPUT-CHANNEL" , "ACL2-USER" , "ACL2"),
1957     ("MAKE-PACKAGE" , "ACL2-USER" , "COMMON-LISP"),
1958     ("MAKE-PATHNAME" , "ACL2-USER" , "COMMON-LISP"),
1959     ("MAKE-RANDOM-STATE" , "ACL2-USER" , "COMMON-LISP"),
1960     ("MAKE-SEQUENCE" , "ACL2-USER" , "COMMON-LISP"),
1961     ("MAKE-STRING" , "ACL2-USER" , "COMMON-LISP"),
1962     ("MAKE-STRING-INPUT-STREAM" , "ACL2-USER" , "COMMON-LISP"),
1963     ("MAKE-STRING-OUTPUT-STREAM" , "ACL2-USER" , "COMMON-LISP"),
1964     ("MAKE-SYMBOL" , "ACL2-USER" , "COMMON-LISP"),
1965     ("MAKE-SYNONYM-STREAM" , "ACL2-USER" , "COMMON-LISP"),
1966     ("MAKE-TWO-WAY-STREAM" , "ACL2-USER" , "COMMON-LISP"),
1967     ("MAKE-VAR-LST" , "ACL2-USER" , "ACL2"),
1968     ("MAKE-VAR-LST1" , "ACL2-USER" , "ACL2"),
2398     ("SET-BOGUS-DEFUN-HINTS-OK" , "ACL2-USER" , "ACL2"),
2832     ("DEFUN" , "MY-PKG" , "COMMON-LISP"),
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"),
3382     ("DEFAULT-DEFUN-MODE" , "U" , "ACL2"),
3383     ("DEFAULT-DEFUN-MODE-FROM-STATE" , "U" , "ACL2"),
3431     ("DEFUN" , "U" , "COMMON-LISP"),
3432     ("DEFUN-NX" , "U" , "ACL2"),
3433     ("DEFUN-SK" , "U" , "ACL2"),
3847     ("MAKE-ARRAY" , "U" , "COMMON-LISP"),
3848     ("MAKE-BROADCAST-STREAM" , "U" , "COMMON-LISP"),
3849     ("MAKE-CHARACTER-LIST" , "U" , "ACL2"),
3850     ("MAKE-CHARACTER-LIST-MAKE-CHARACTER-LIST" , "U" , "ACL2"),
3851     ("MAKE-CONCATENATED-STREAM" , "U" , "COMMON-LISP"),
3852     ("MAKE-CONDITION" , "U" , "COMMON-LISP"),
3853     ("MAKE-DISPATCH-MACRO-CHARACTER" , "U" , "COMMON-LISP"),
3854     ("MAKE-ECHO-STREAM" , "U" , "COMMON-LISP"),
3855     ("MAKE-EVENT" , "U" , "ACL2"),
3856     ("MAKE-FMT-BINDINGS" , "U" , "ACL2"),
3857     ("MAKE-HASH-TABLE" , "U" , "COMMON-LISP"),
3858     ("MAKE-INPUT-CHANNEL" , "U" , "ACL2"),
3859     ("MAKE-INSTANCE" , "U" , "COMMON-LISP"),
3860     ("MAKE-INSTANCES-OBSOLETE" , "U" , "COMMON-LISP"),
3861     ("MAKE-LIST" , "U" , "COMMON-LISP"),
3862     ("MAKE-LIST-AC" , "U" , "ACL2"),
3863     ("MAKE-LOAD-FORM" , "U" , "COMMON-LISP"),
3864     ("MAKE-LOAD-FORM-SAVING-SLOTS" , "U" , "COMMON-LISP"),
3865     ("MAKE-METHOD" , "U" , "COMMON-LISP"),
3866     ("MAKE-MV-NTHS" , "U" , "ACL2"),
3867     ("MAKE-ORD" , "U" , "ACL2"),
3868     ("MAKE-OUTPUT-CHANNEL" , "U" , "ACL2"),
3869     ("MAKE-PACKAGE" , "U" , "COMMON-LISP"),
3870     ("MAKE-PATHNAME" , "U" , "COMMON-LISP"),
3871     ("MAKE-RANDOM-STATE" , "U" , "COMMON-LISP"),
3872     ("MAKE-SEQUENCE" , "U" , "COMMON-LISP"),
3873     ("MAKE-STRING" , "U" , "COMMON-LISP"),
3874     ("MAKE-STRING-INPUT-STREAM" , "U" , "COMMON-LISP"),
3875     ("MAKE-STRING-OUTPUT-STREAM" , "U" , "COMMON-LISP"),
3876     ("MAKE-SYMBOL" , "U" , "COMMON-LISP"),
3877     ("MAKE-SYNONYM-STREAM" , "U" , "COMMON-LISP"),
3878     ("MAKE-TWO-WAY-STREAM" , "U" , "COMMON-LISP"),
3879     ("MAKE-VAR-LST" , "U" , "ACL2"),
3880     ("MAKE-VAR-LST1" , "U" , "ACL2"),
4304     ("SET-BOGUS-DEFUN-HINTS-OK" , "U" , "ACL2"),
5219     ("DEFAULT-DEFUN-MODE" , "ACL2-ASG" , "ACL2"),
5220     ("DEFAULT-DEFUN-MODE-FROM-STATE" , "ACL2-ASG" , "ACL2"),
5268     ("DEFUN" , "ACL2-ASG" , "COMMON-LISP"),
5269     ("DEFUN-NX" , "ACL2-ASG" , "ACL2"),
5270     ("DEFUN-SK" , "ACL2-ASG" , "ACL2"),
5684     ("MAKE-ARRAY" , "ACL2-ASG" , "COMMON-LISP"),
5685     ("MAKE-BROADCAST-STREAM" , "ACL2-ASG" , "COMMON-LISP"),
5686     ("MAKE-CHARACTER-LIST" , "ACL2-ASG" , "ACL2"),
5687     ("MAKE-CHARACTER-LIST-MAKE-CHARACTER-LIST" , "ACL2-ASG" , "ACL2"),
5688     ("MAKE-CONCATENATED-STREAM" , "ACL2-ASG" , "COMMON-LISP"),
5689     ("MAKE-CONDITION" , "ACL2-ASG" , "COMMON-LISP"),
5690     ("MAKE-DISPATCH-MACRO-CHARACTER" , "ACL2-ASG" , "COMMON-LISP"),
5691     ("MAKE-ECHO-STREAM" , "ACL2-ASG" , "COMMON-LISP"),
5692     ("MAKE-EVENT" , "ACL2-ASG" , "ACL2"),
5693     ("MAKE-FMT-BINDINGS" , "ACL2-ASG" , "ACL2"),
5694     ("MAKE-HASH-TABLE" , "ACL2-ASG" , "COMMON-LISP"),
5695     ("MAKE-INPUT-CHANNEL" , "ACL2-ASG" , "ACL2"),
5696     ("MAKE-INSTANCE" , "ACL2-ASG" , "COMMON-LISP"),
5697     ("MAKE-INSTANCES-OBSOLETE" , "ACL2-ASG" , "COMMON-LISP"),
5698     ("MAKE-LIST" , "ACL2-ASG" , "COMMON-LISP"),
5699     ("MAKE-LIST-AC" , "ACL2-ASG" , "ACL2"),
5700     ("MAKE-LOAD-FORM" , "ACL2-ASG" , "COMMON-LISP"),
5701     ("MAKE-LOAD-FORM-SAVING-SLOTS" , "ACL2-ASG" , "COMMON-LISP"),
5702     ("MAKE-METHOD" , "ACL2-ASG" , "COMMON-LISP"),
5703     ("MAKE-MV-NTHS" , "ACL2-ASG" , "ACL2"),
5704     ("MAKE-ORD" , "ACL2-ASG" , "ACL2"),
5705     ("MAKE-OUTPUT-CHANNEL" , "ACL2-ASG" , "ACL2"),
5706     ("MAKE-PACKAGE" , "ACL2-ASG" , "COMMON-LISP"),
5707     ("MAKE-PATHNAME" , "ACL2-ASG" , "COMMON-LISP"),
5708     ("MAKE-RANDOM-STATE" , "ACL2-ASG" , "COMMON-LISP"),
5709     ("MAKE-SEQUENCE" , "ACL2-ASG" , "COMMON-LISP"),
5710     ("MAKE-STRING" , "ACL2-ASG" , "COMMON-LISP"),
5711     ("MAKE-STRING-INPUT-STREAM" , "ACL2-ASG" , "COMMON-LISP"),
5712     ("MAKE-STRING-OUTPUT-STREAM" , "ACL2-ASG" , "COMMON-LISP"),
5713     ("MAKE-SYMBOL" , "ACL2-ASG" , "COMMON-LISP"),
5714     ("MAKE-SYNONYM-STREAM" , "ACL2-ASG" , "COMMON-LISP"),
5715     ("MAKE-TWO-WAY-STREAM" , "ACL2-ASG" , "COMMON-LISP"),
5716     ("MAKE-VAR-LST" , "ACL2-ASG" , "ACL2"),
5717     ("MAKE-VAR-LST1" , "ACL2-ASG" , "ACL2"),
6147     ("SET-BOGUS-DEFUN-HINTS-OK" , "ACL2-ASG" , "ACL2"),
7068     ("DEFAULT-DEFUN-MODE" , "ACL2-AGP" , "ACL2"),
7069     ("DEFAULT-DEFUN-MODE-FROM-STATE" , "ACL2-AGP" , "ACL2"),
7117     ("DEFUN" , "ACL2-AGP" , "COMMON-LISP"),
7118     ("DEFUN-NX" , "ACL2-AGP" , "ACL2"),
7119     ("DEFUN-SK" , "ACL2-AGP" , "ACL2"),
7533     ("MAKE-ARRAY" , "ACL2-AGP" , "COMMON-LISP"),
7534     ("MAKE-BROADCAST-STREAM" , "ACL2-AGP" , "COMMON-LISP"),
7535     ("MAKE-CHARACTER-LIST" , "ACL2-AGP" , "ACL2"),
7536     ("MAKE-CHARACTER-LIST-MAKE-CHARACTER-LIST" , "ACL2-AGP" , "ACL2"),
7537     ("MAKE-CONCATENATED-STREAM" , "ACL2-AGP" , "COMMON-LISP"),
7538     ("MAKE-CONDITION" , "ACL2-AGP" , "COMMON-LISP"),
7539     ("MAKE-DISPATCH-MACRO-CHARACTER" , "ACL2-AGP" , "COMMON-LISP"),
7540     ("MAKE-ECHO-STREAM" , "ACL2-AGP" , "COMMON-LISP"),
7541     ("MAKE-EVENT" , "ACL2-AGP" , "ACL2"),
7542     ("MAKE-FMT-BINDINGS" , "ACL2-AGP" , "ACL2"),
7543     ("MAKE-HASH-TABLE" , "ACL2-AGP" , "COMMON-LISP"),
7544     ("MAKE-INPUT-CHANNEL" , "ACL2-AGP" , "ACL2"),
7545     ("MAKE-INSTANCE" , "ACL2-AGP" , "COMMON-LISP"),
7546     ("MAKE-INSTANCES-OBSOLETE" , "ACL2-AGP" , "COMMON-LISP"),
7547     ("MAKE-LIST" , "ACL2-AGP" , "COMMON-LISP"),
7548     ("MAKE-LIST-AC" , "ACL2-AGP" , "ACL2"),
7549     ("MAKE-LOAD-FORM" , "ACL2-AGP" , "COMMON-LISP"),
7550     ("MAKE-LOAD-FORM-SAVING-SLOTS" , "ACL2-AGP" , "COMMON-LISP"),
7551     ("MAKE-METHOD" , "ACL2-AGP" , "COMMON-LISP"),
7552     ("MAKE-MV-NTHS" , "ACL2-AGP" , "ACL2"),
7553     ("MAKE-ORD" , "ACL2-AGP" , "ACL2"),
7554     ("MAKE-OUTPUT-CHANNEL" , "ACL2-AGP" , "ACL2"),
7555     ("MAKE-PACKAGE" , "ACL2-AGP" , "COMMON-LISP"),
7556     ("MAKE-PATHNAME" , "ACL2-AGP" , "COMMON-LISP"),
7557     ("MAKE-RANDOM-STATE" , "ACL2-AGP" , "COMMON-LISP"),
7558     ("MAKE-SEQUENCE" , "ACL2-AGP" , "COMMON-LISP"),
7559     ("MAKE-STRING" , "ACL2-AGP" , "COMMON-LISP"),
7560     ("MAKE-STRING-INPUT-STREAM" , "ACL2-AGP" , "COMMON-LISP"),
7561     ("MAKE-STRING-OUTPUT-STREAM" , "ACL2-AGP" , "COMMON-LISP"),
7562     ("MAKE-SYMBOL" , "ACL2-AGP" , "COMMON-LISP"),
7563     ("MAKE-SYNONYM-STREAM" , "ACL2-AGP" , "COMMON-LISP"),
7564     ("MAKE-TWO-WAY-STREAM" , "ACL2-AGP" , "COMMON-LISP"),
7565     ("MAKE-VAR-LST" , "ACL2-AGP" , "ACL2"),
7566     ("MAKE-VAR-LST1" , "ACL2-AGP" , "ACL2"),
7996     ("SET-BOGUS-DEFUN-HINTS-OK" , "ACL2-AGP" , "ACL2"),
8917     ("DEFAULT-DEFUN-MODE" , "ACL2-CRG" , "ACL2"),
8918     ("DEFAULT-DEFUN-MODE-FROM-STATE" , "ACL2-CRG" , "ACL2"),
8966     ("DEFUN" , "ACL2-CRG" , "COMMON-LISP"),
8967     ("DEFUN-NX" , "ACL2-CRG" , "ACL2"),
8968     ("DEFUN-SK" , "ACL2-CRG" , "ACL2"),
9382     ("MAKE-ARRAY" , "ACL2-CRG" , "COMMON-LISP"),
9383     ("MAKE-BROADCAST-STREAM" , "ACL2-CRG" , "COMMON-LISP"),
9384     ("MAKE-CHARACTER-LIST" , "ACL2-CRG" , "ACL2"),
9385     ("MAKE-CHARACTER-LIST-MAKE-CHARACTER-LIST" , "ACL2-CRG" , "ACL2"),
9386     ("MAKE-CONCATENATED-STREAM" , "ACL2-CRG" , "COMMON-LISP"),
9387     ("MAKE-CONDITION" , "ACL2-CRG" , "COMMON-LISP"),
9388     ("MAKE-DISPATCH-MACRO-CHARACTER" , "ACL2-CRG" , "COMMON-LISP"),
9389     ("MAKE-ECHO-STREAM" , "ACL2-CRG" , "COMMON-LISP"),
9390     ("MAKE-EVENT" , "ACL2-CRG" , "ACL2"),
9391     ("MAKE-FMT-BINDINGS" , "ACL2-CRG" , "ACL2"),
9392     ("MAKE-HASH-TABLE" , "ACL2-CRG" , "COMMON-LISP"),
9393     ("MAKE-INPUT-CHANNEL" , "ACL2-CRG" , "ACL2"),
9394     ("MAKE-INSTANCE" , "ACL2-CRG" , "COMMON-LISP"),
9395     ("MAKE-INSTANCES-OBSOLETE" , "ACL2-CRG" , "COMMON-LISP"),
9396     ("MAKE-LIST" , "ACL2-CRG" , "COMMON-LISP"),
9397     ("MAKE-LIST-AC" , "ACL2-CRG" , "ACL2"),
9398     ("MAKE-LOAD-FORM" , "ACL2-CRG" , "COMMON-LISP"),
9399     ("MAKE-LOAD-FORM-SAVING-SLOTS" , "ACL2-CRG" , "COMMON-LISP"),
9400     ("MAKE-METHOD" , "ACL2-CRG" , "COMMON-LISP"),
9401     ("MAKE-MV-NTHS" , "ACL2-CRG" , "ACL2"),
9402     ("MAKE-ORD" , "ACL2-CRG" , "ACL2"),
9403     ("MAKE-OUTPUT-CHANNEL" , "ACL2-CRG" , "ACL2"),
9404     ("MAKE-PACKAGE" , "ACL2-CRG" , "COMMON-LISP"),
9405     ("MAKE-PATHNAME" , "ACL2-CRG" , "COMMON-LISP"),
9406     ("MAKE-RANDOM-STATE" , "ACL2-CRG" , "COMMON-LISP"),
9407     ("MAKE-SEQUENCE" , "ACL2-CRG" , "COMMON-LISP"),
9408     ("MAKE-STRING" , "ACL2-CRG" , "COMMON-LISP"),
9409     ("MAKE-STRING-INPUT-STREAM" , "ACL2-CRG" , "COMMON-LISP"),
9410     ("MAKE-STRING-OUTPUT-STREAM" , "ACL2-CRG" , "COMMON-LISP"),
9411     ("MAKE-SYMBOL" , "ACL2-CRG" , "COMMON-LISP"),
9412     ("MAKE-SYNONYM-STREAM" , "ACL2-CRG" , "COMMON-LISP"),
9413     ("MAKE-TWO-WAY-STREAM" , "ACL2-CRG" , "COMMON-LISP"),
9414     ("MAKE-VAR-LST" , "ACL2-CRG" , "ACL2"),
9415     ("MAKE-VAR-LST1" , "ACL2-CRG" , "ACL2"),
9845     ("SET-BOGUS-DEFUN-HINTS-OK" , "ACL2-CRG" , "ACL2"),
10284     "M1",