tests/inputs/PKGS.sml

963     ("UPDATE-INSTANCE-FOR-DIFFERENT-CLASS" , "ACL2" , "COMMON-LISP"),
965     ("UPDATE-INSTANCE-FOR-REDEFINED-CLASS" , "ACL2" , "COMMON-LISP"),
1875     ("LEN-UPDATE-NTH" , "ACL2-USER" , "ACL2"),
2080     ("NTH-UPDATE-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"),
3787     ("LEN-UPDATE-NTH" , "U" , "ACL2"),
3992     ("NTH-UPDATE-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"),
5624     ("LEN-UPDATE-NTH" , "ACL2-ASG" , "ACL2"),
5829     ("NTH-UPDATE-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"),
7473     ("LEN-UPDATE-NTH" , "ACL2-AGP" , "ACL2"),
7678     ("NTH-UPDATE-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"),
9322     ("LEN-UPDATE-NTH" , "ACL2-CRG" , "ACL2"),
9527     ("NTH-UPDATE-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"),