Lines Matching refs:UPDATE
2782 [oracles: DEFUN ACL2::UPDATE-NTH, DISK_THM] [axioms: ] []
2789 [oracles: DEFUN ACL2::UPDATE-NTH-ARRAY] [axioms: ] []
2831 [oracles: DEFUN ACL2::UPDATE-OPEN-INPUT-CHANNELS, DISK_THM] [axioms: ]
2841 [oracles: DEFUN ACL2::UPDATE-OPEN-OUTPUT-CHANNELS, DISK_THM] [axioms: ]
2851 [oracles: DEFUN ACL2::UPDATE-GLOBAL-TABLE, DISK_THM] [axioms: ] []
2861 [oracles: DEFUN ACL2::UPDATE-T-STACK, DISK_THM] [axioms: ] []
2871 [oracles: DEFUN ACL2::UPDATE-32-BIT-INTEGER-STACK, DISK_THM] [axioms: ]
2881 [oracles: DEFUN ACL2::UPDATE-BIG-CLOCK-ENTRY, DISK_THM] [axioms: ] []
2891 [oracles: DEFUN ACL2::UPDATE-IDATES, DISK_THM] [axioms: ] []
2901 [oracles: DEFUN ACL2::UPDATE-RUN-TIMES, DISK_THM] [axioms: ] []
2911 [oracles: DEFUN ACL2::UPDATE-FILE-CLOCK, DISK_THM] [axioms: ] []
2926 [oracles: DEFUN ACL2::UPDATE-WRITTEN-FILES, DISK_THM] [axioms: ] []
2936 [oracles: DEFUN ACL2::UPDATE-READ-FILES, DISK_THM] [axioms: ] []
2951 [oracles: DEFUN ACL2::UPDATE-LIST-ALL-PACKAGE-NAMES-LST, DISK_THM]
2962 [oracles: DEFUN ACL2::UPDATE-USER-STOBJ-ALIST1, DISK_THM] [axioms: ] []
4000 [oracles: DEFUN ACL2::UPDATE-USER-STOBJ-ALIST] [axioms: ] []