tests/inputs/PKGS.sml

178     ("ASSOC" , "ACL2" , "COMMON-LISP"),
181     ("ASSOC-IF" , "ACL2" , "COMMON-LISP"),
184     ("ASSOC-IF-NOT" , "ACL2" , "COMMON-LISP"),
1105     ("ALL-BOUNDP-PRESERVES-ASSOC" , "ACL2-USER" , "ACL2"),
1160     ("ASSOC" , "ACL2-USER" , "COMMON-LISP"),
1161     ("ASSOC-ADD-PAIR" , "ACL2-USER" , "ACL2"),
1162     ("ASSOC-EQ" , "ACL2-USER" , "ACL2"),
1163     ("ASSOC-EQ-EQUAL" , "ACL2-USER" , "ACL2"),
1164     ("ASSOC-EQ-EQUAL-ALISTP" , "ACL2-USER" , "ACL2"),
1165     ("ASSOC-EQUAL" , "ACL2-USER" , "ACL2"),
1166     ("ASSOC-IF" , "ACL2-USER" , "COMMON-LISP"),
1167     ("ASSOC-IF-NOT" , "ACL2-USER" , "COMMON-LISP"),
1168     ("ASSOC-KEYWORD" , "ACL2-USER" , "ACL2"),
1169     ("ASSOC-STRING-EQUAL" , "ACL2-USER" , "ACL2"),
1421     ("CONSP-ASSOC" , "ACL2-USER" , "ACL2"),
1422     ("CONSP-ASSOC-EQ" , "ACL2-USER" , "ACL2"),
1828     ("KEYWORD-VALUE-LISTP-ASSOC-KEYWORD" , "ACL2-USER" , "ACL2"),
2179     ("PLIST-WORLDP-FORWARD-TO-ASSOC-EQ-EQUAL-ALISTP" , "ACL2-USER"
2257     ("PUT-ASSOC-EQ" , "ACL2-USER" , "ACL2"),
2258     ("PUT-ASSOC-EQUAL" , "ACL2-USER" , "ACL2"),
2682     ("TRUE-LIST-LISTP-FORWARD-TO-TRUE-LISTP-ASSOC-EQ" , "ACL2-USER"
2685     ("TRUE-LISTP-CADR-ASSOC-EQ-FOR-OPEN-CHANNELS-P" , "ACL2-USER" ,
2844     ("ASSOC" , "M1" , "COMMON-LISP"),
3018     ("ALL-BOUNDP-PRESERVES-ASSOC" , "U" , "ACL2"),
3073     ("ASSOC" , "U" , "COMMON-LISP"),
3074     ("ASSOC-ADD-PAIR" , "U" , "ACL2"),
3075     ("ASSOC-EQ" , "U" , "ACL2"),
3076     ("ASSOC-EQ-EQUAL" , "U" , "ACL2"),
3077     ("ASSOC-EQ-EQUAL-ALISTP" , "U" , "ACL2"),
3078     ("ASSOC-EQUAL" , "U" , "ACL2"),
3079     ("ASSOC-IF" , "U" , "COMMON-LISP"),
3080     ("ASSOC-IF-NOT" , "U" , "COMMON-LISP"),
3081     ("ASSOC-KEYWORD" , "U" , "ACL2"),
3082     ("ASSOC-STRING-EQUAL" , "U" , "ACL2"),
3333     ("CONSP-ASSOC" , "U" , "ACL2"),
3334     ("CONSP-ASSOC-EQ" , "U" , "ACL2"),
3740     ("KEYWORD-VALUE-LISTP-ASSOC-KEYWORD" , "U" , "ACL2"),
4089     ("PLIST-WORLDP-FORWARD-TO-ASSOC-EQ-EQUAL-ALISTP" , "U" , "ACL2"),
4166     ("PUT-ASSOC-EQ" , "U" , "ACL2"),
4167     ("PUT-ASSOC-EQUAL" , "U" , "ACL2"),
4587     ("TRUE-LIST-LISTP-FORWARD-TO-TRUE-LISTP-ASSOC-EQ" , "U" , "ACL2"),
4589     ("TRUE-LISTP-CADR-ASSOC-EQ-FOR-OPEN-CHANNELS-P" , "U" , "ACL2"),
4854     ("ALL-BOUNDP-PRESERVES-ASSOC" , "ACL2-ASG" , "ACL2"),
4909     ("ASSOC" , "ACL2-ASG" , "COMMON-LISP"),
4910     ("ASSOC-ADD-PAIR" , "ACL2-ASG" , "ACL2"),
4911     ("ASSOC-EQ" , "ACL2-ASG" , "ACL2"),
4912     ("ASSOC-EQ-EQUAL" , "ACL2-ASG" , "ACL2"),
4913     ("ASSOC-EQ-EQUAL-ALISTP" , "ACL2-ASG" , "ACL2"),
4914     ("ASSOC-EQUAL" , "ACL2-ASG" , "ACL2"),
4915     ("ASSOC-IF" , "ACL2-ASG" , "COMMON-LISP"),
4916     ("ASSOC-IF-NOT" , "ACL2-ASG" , "COMMON-LISP"),
4917     ("ASSOC-KEYWORD" , "ACL2-ASG" , "ACL2"),
4918     ("ASSOC-STRING-EQUAL" , "ACL2-ASG" , "ACL2"),
5170     ("CONSP-ASSOC" , "ACL2-ASG" , "ACL2"),
5171     ("CONSP-ASSOC-EQ" , "ACL2-ASG" , "ACL2"),
5577     ("KEYWORD-VALUE-LISTP-ASSOC-KEYWORD" , "ACL2-ASG" , "ACL2"),
5928     ("PLIST-WORLDP-FORWARD-TO-ASSOC-EQ-EQUAL-ALISTP" , "ACL2-ASG" ,
6006     ("PUT-ASSOC-EQ" , "ACL2-ASG" , "ACL2"),
6007     ("PUT-ASSOC-EQUAL" , "ACL2-ASG" , "ACL2"),
6431     ("TRUE-LIST-LISTP-FORWARD-TO-TRUE-LISTP-ASSOC-EQ" , "ACL2-ASG"
6434     ("TRUE-LISTP-CADR-ASSOC-EQ-FOR-OPEN-CHANNELS-P" , "ACL2-ASG" ,
6703     ("ALL-BOUNDP-PRESERVES-ASSOC" , "ACL2-AGP" , "ACL2"),
6758     ("ASSOC" , "ACL2-AGP" , "COMMON-LISP"),
6759     ("ASSOC-ADD-PAIR" , "ACL2-AGP" , "ACL2"),
6760     ("ASSOC-EQ" , "ACL2-AGP" , "ACL2"),
6761     ("ASSOC-EQ-EQUAL" , "ACL2-AGP" , "ACL2"),
6762     ("ASSOC-EQ-EQUAL-ALISTP" , "ACL2-AGP" , "ACL2"),
6763     ("ASSOC-EQUAL" , "ACL2-AGP" , "ACL2"),
6764     ("ASSOC-IF" , "ACL2-AGP" , "COMMON-LISP"),
6765     ("ASSOC-IF-NOT" , "ACL2-AGP" , "COMMON-LISP"),
6766     ("ASSOC-KEYWORD" , "ACL2-AGP" , "ACL2"),
6767     ("ASSOC-STRING-EQUAL" , "ACL2-AGP" , "ACL2"),
7019     ("CONSP-ASSOC" , "ACL2-AGP" , "ACL2"),
7020     ("CONSP-ASSOC-EQ" , "ACL2-AGP" , "ACL2"),
7426     ("KEYWORD-VALUE-LISTP-ASSOC-KEYWORD" , "ACL2-AGP" , "ACL2"),
7777     ("PLIST-WORLDP-FORWARD-TO-ASSOC-EQ-EQUAL-ALISTP" , "ACL2-AGP" ,
7855     ("PUT-ASSOC-EQ" , "ACL2-AGP" , "ACL2"),
7856     ("PUT-ASSOC-EQUAL" , "ACL2-AGP" , "ACL2"),
8280     ("TRUE-LIST-LISTP-FORWARD-TO-TRUE-LISTP-ASSOC-EQ" , "ACL2-AGP"
8283     ("TRUE-LISTP-CADR-ASSOC-EQ-FOR-OPEN-CHANNELS-P" , "ACL2-AGP" ,
8552     ("ALL-BOUNDP-PRESERVES-ASSOC" , "ACL2-CRG" , "ACL2"),
8607     ("ASSOC" , "ACL2-CRG" , "COMMON-LISP"),
8608     ("ASSOC-ADD-PAIR" , "ACL2-CRG" , "ACL2"),
8609     ("ASSOC-EQ" , "ACL2-CRG" , "ACL2"),
8610     ("ASSOC-EQ-EQUAL" , "ACL2-CRG" , "ACL2"),
8611     ("ASSOC-EQ-EQUAL-ALISTP" , "ACL2-CRG" , "ACL2"),
8612     ("ASSOC-EQUAL" , "ACL2-CRG" , "ACL2"),
8613     ("ASSOC-IF" , "ACL2-CRG" , "COMMON-LISP"),
8614     ("ASSOC-IF-NOT" , "ACL2-CRG" , "COMMON-LISP"),
8615     ("ASSOC-KEYWORD" , "ACL2-CRG" , "ACL2"),
8616     ("ASSOC-STRING-EQUAL" , "ACL2-CRG" , "ACL2"),
8868     ("CONSP-ASSOC" , "ACL2-CRG" , "ACL2"),
8869     ("CONSP-ASSOC-EQ" , "ACL2-CRG" , "ACL2"),
9275     ("KEYWORD-VALUE-LISTP-ASSOC-KEYWORD" , "ACL2-CRG" , "ACL2"),
9626     ("PLIST-WORLDP-FORWARD-TO-ASSOC-EQ-EQUAL-ALISTP" , "ACL2-CRG" ,
9704     ("PUT-ASSOC-EQ" , "ACL2-CRG" , "ACL2"),
9705     ("PUT-ASSOC-EQUAL" , "ACL2-CRG" , "ACL2"),
10129     ("TRUE-LIST-LISTP-FORWARD-TO-TRUE-LISTP-ASSOC-EQ" , "ACL2-CRG"
10132     ("TRUE-LISTP-CADR-ASSOC-EQ-FOR-OPEN-CHANNELS-P" , "ACL2-CRG" ,