Lines Matching refs:UPDATE
484 ("LEN-UPDATE-NTH", "ACL2-USER", "ACL2"),
542 ("NTH-UPDATE-NTH", "ACL2-USER", "ACL2"),
735 ("STATE-P1-UPDATE-MAIN-TIMER", "ACL2-USER", "ACL2"),
736 ("STATE-P1-UPDATE-NTH-2-WORLD", "ACL2-USER", "ACL2"),
803 ("TRUE-LISTP-UPDATE-NTH", "ACL2-USER", "ACL2"),
821 ("UPDATE-32-BIT-INTEGER-STACK", "ACL2-USER", "ACL2"),
822 ("UPDATE-BIG-CLOCK-ENTRY", "ACL2-USER", "ACL2"),
823 ("UPDATE-FILE-CLOCK", "ACL2-USER", "ACL2"),
824 ("UPDATE-GLOBAL-TABLE", "ACL2-USER", "ACL2"),
825 ("UPDATE-IDATES", "ACL2-USER", "ACL2"),
826 ("UPDATE-LIST-ALL-PACKAGE-NAMES-LST", "ACL2-USER", "ACL2"),
827 ("UPDATE-NTH", "ACL2-USER", "ACL2"),
828 ("UPDATE-OPEN-INPUT-CHANNELS", "ACL2-USER", "ACL2"),
829 ("UPDATE-OPEN-OUTPUT-CHANNELS", "ACL2-USER", "ACL2"),
830 ("UPDATE-READ-FILES", "ACL2-USER", "ACL2"),
831 ("UPDATE-RUN-TIMES", "ACL2-USER", "ACL2"),
832 ("UPDATE-RUN-TIMES-PRESERVES-STATE-P1", "ACL2-USER", "ACL2"),
833 ("UPDATE-T-STACK", "ACL2-USER", "ACL2"),
834 ("UPDATE-USER-STOBJ-ALIST", "ACL2-USER", "ACL2"),
835 ("UPDATE-USER-STOBJ-ALIST1", "ACL2-USER", "ACL2"),
836 ("UPDATE-WRITTEN-FILES", "ACL2-USER", "ACL2"),
1836 ("UPDATE-INSTANCE-FOR-DIFFERENT-CLASS", "ACL2-USER", "COMMON-LISP"),
1838 ("UPDATE-INSTANCE-FOR-REDEFINED-CLASS", "ACL2-USER", "COMMON-LISP"),
2814 ("UPDATE-INSTANCE-FOR-DIFFERENT-CLASS", "ACL2", "COMMON-LISP"),
2816 ("UPDATE-INSTANCE-FOR-REDEFINED-CLASS", "ACL2", "COMMON-LISP"),