Lines Matching refs:UPDATE
2786 [oracles: DEFUN ACL2::UPDATE-NTH, DISK_THM] [axioms: ] []
2793 [oracles: DEFUN ACL2::UPDATE-NTH-ARRAY] [axioms: ] []
2835 [oracles: DEFUN ACL2::UPDATE-OPEN-INPUT-CHANNELS, DISK_THM] [axioms: ]
2845 [oracles: DEFUN ACL2::UPDATE-OPEN-OUTPUT-CHANNELS, DISK_THM] [axioms: ]
2855 [oracles: DEFUN ACL2::UPDATE-GLOBAL-TABLE, DISK_THM] [axioms: ] []
2865 [oracles: DEFUN ACL2::UPDATE-T-STACK, DISK_THM] [axioms: ] []
2875 [oracles: DEFUN ACL2::UPDATE-32-BIT-INTEGER-STACK, DISK_THM] [axioms: ]
2885 [oracles: DEFUN ACL2::UPDATE-BIG-CLOCK-ENTRY, DISK_THM] [axioms: ] []
2895 [oracles: DEFUN ACL2::UPDATE-IDATES, DISK_THM] [axioms: ] []
2905 [oracles: DEFUN ACL2::UPDATE-RUN-TIMES, DISK_THM] [axioms: ] []
2915 [oracles: DEFUN ACL2::UPDATE-FILE-CLOCK, DISK_THM] [axioms: ] []
2930 [oracles: DEFUN ACL2::UPDATE-WRITTEN-FILES, DISK_THM] [axioms: ] []
2940 [oracles: DEFUN ACL2::UPDATE-READ-FILES, DISK_THM] [axioms: ] []
2955 [oracles: DEFUN ACL2::UPDATE-LIST-ALL-PACKAGE-NAMES-LST, DISK_THM]
2966 [oracles: DEFUN ACL2::UPDATE-USER-STOBJ-ALIST1, DISK_THM] [axioms: ] []
4004 [oracles: DEFUN ACL2::UPDATE-USER-STOBJ-ALIST] [axioms: ] []