Lines Matching defs:GLOBAL

1745                      (CONS (CONS 'F-GET-GLOBAL
1757 (CONS 'STATE-GLOBAL-LET*
2781 GLOBAL-VAL (VAR WRLD)
2783 VAR 'GLOBAL-VALUE
2785 "GLOBAL-VAL didn't find a value. Initialize this ~
3437 (DEFUN GLOBAL-TABLE (ST) (NTH '2 ST))
3439 (DEFUN UPDATE-GLOBAL-TABLE (X ST) (UPDATE-NTH '2 X ST))
3798 (ORDERED-SYMBOL-ALISTP (GLOBAL-TABLE X))
3832 (GLOBAL-ENABLED-STRUCTURE)
3878 PUT-GLOBAL CLOSE-INPUT-CHANNEL
3879 MAKUNBOUND-GLOBAL OPEN-INPUT-CHANNEL-P1
3880 BOUNDP-GLOBAL1 GLOBAL-TABLE-CARS1
3884 GET-GLOBAL 32-BIT-INTEGER-STACK-LENGTH1
3924 PROGN! F-PUT-GLOBAL PUSH-UNTOUCHABLE
3954 SKIP-PROOFS F-BOUNDP-GLOBAL
3959 DEFDOC PUSH-GFRAME DEFTHMD F-GET-GLOBAL
4016 RECOMPRESS-GLOBAL-ENABLED-STRUCTURE EV-W
4102 (GLOBAL-TABLE X))
4105 (GLOBAL-TABLE X))))
4111 (GLOBAL-TABLE X)))))
4113 (TIMER-ALISTP (CDR (ASSOC 'TIMER-ALIST (GLOBAL-TABLE X))))
4116 'GLOBAL-VALUE
4119 (GLOBAL-TABLE X)))))
4210 (GLOBAL-ENABLED-STRUCTURE)
4256 PUT-GLOBAL CLOSE-INPUT-CHANNEL
4257 MAKUNBOUND-GLOBAL OPEN-INPUT-CHANNEL-P1
4258 BOUNDP-GLOBAL1 GLOBAL-TABLE-CARS1
4262 GET-GLOBAL 32-BIT-INTEGER-STACK-LENGTH1
4302 PROGN! F-PUT-GLOBAL PUSH-UNTOUCHABLE
4332 SKIP-PROOFS F-BOUNDP-GLOBAL
4337 DEFDOC PUSH-GFRAME DEFTHMD F-GET-GLOBAL
4394 RECOMPRESS-GLOBAL-ENABLED-STRUCTURE EV-W
4493 'GLOBAL-VALUE
4543 GLOBAL-TABLE T-STACK
4586 (GLOBAL-ENABLED-STRUCTURE)
4632 PUT-GLOBAL CLOSE-INPUT-CHANNEL
4633 MAKUNBOUND-GLOBAL OPEN-INPUT-CHANNEL-P1
4634 BOUNDP-GLOBAL1 GLOBAL-TABLE-CARS1
4638 GET-GLOBAL 32-BIT-INTEGER-STACK-LENGTH1
4678 PROGN! F-PUT-GLOBAL PUSH-UNTOUCHABLE
4708 SKIP-PROOFS F-BOUNDP-GLOBAL
4713 DEFDOC PUSH-GFRAME DEFTHMD F-GET-GLOBAL
4770 RECOMPRESS-GLOBAL-ENABLED-STRUCTURE EV-W
4863 GLOBAL-TABLE
4889 (DEFUN GLOBAL-TABLE-CARS1 (STATE-STATE)
4890 (STRIP-CARS (GLOBAL-TABLE STATE-STATE)))
4892 (DEFUN GLOBAL-TABLE-CARS (STATE-STATE) (GLOBAL-TABLE-CARS1 STATE-STATE))
4895 (IF (ASSOC X (GLOBAL-TABLE STATE-STATE))
4899 (DEFUN BOUNDP-GLOBAL (X STATE-STATE) (BOUNDP-GLOBAL1 X STATE-STATE))
4909 (DEFUN MAKUNBOUND-GLOBAL (X STATE-STATE)
4910 (UPDATE-GLOBAL-TABLE (DELETE-PAIR X (GLOBAL-TABLE STATE-STATE))
4913 (DEFUN GET-GLOBAL (X STATE-STATE)
4914 (CDR (ASSOC X (GLOBAL-TABLE STATE-STATE))))
4916 (DEFUN PUT-GLOBAL (KEY VALUE STATE-STATE)
4917 (UPDATE-GLOBAL-TABLE (ADD-PAIR KEY VALUE (GLOBAL-TABLE STATE-STATE))
4934 ALWAYS-BOUNDP-GLOBAL (X)
4969 (GLOBAL-ENABLED-STRUCTURE)
5015 PUT-GLOBAL CLOSE-INPUT-CHANNEL
5016 MAKUNBOUND-GLOBAL OPEN-INPUT-CHANNEL-P1
5017 BOUNDP-GLOBAL1 GLOBAL-TABLE-CARS1
5021 GET-GLOBAL 32-BIT-INTEGER-STACK-LENGTH1
5061 PROGN! F-PUT-GLOBAL PUSH-UNTOUCHABLE
5091 SKIP-PROOFS F-BOUNDP-GLOBAL
5096 DEFDOC PUSH-GFRAME DEFTHMD F-GET-GLOBAL
5152 RECOMPRESS-GLOBAL-ENABLED-STRUCTURE EV-W
5271 (GLOBAL-ENABLED-STRUCTURE)
5317 PUT-GLOBAL CLOSE-INPUT-CHANNEL
5318 MAKUNBOUND-GLOBAL OPEN-INPUT-CHANNEL-P1
5319 BOUNDP-GLOBAL1 GLOBAL-TABLE-CARS1
5323 GET-GLOBAL 32-BIT-INTEGER-STACK-LENGTH1
5363 PROGN! F-PUT-GLOBAL PUSH-UNTOUCHABLE
5393 SKIP-PROOFS F-BOUNDP-GLOBAL
5398 DEFDOC PUSH-GFRAME DEFTHMD F-GET-GLOBAL
5454 RECOMPRESS-GLOBAL-ENABLED-STRUCTURE EV-W
5565 (DEFUN STATE-GLOBAL-LET*-BINDINGS-P (LST)
5578 (STATE-GLOBAL-LET*-BINDINGS-P (CDR LST))
5585 STATE-GLOBAL-LET*-GET-GLOBALS (BINDINGS)
5591 (ALWAYS-BOUNDP-GLOBAL (CAR (CAR BINDINGS)))
5593 (CONS (CONS 'F-GET-GLOBAL
5601 (CONS 'F-BOUNDP-GLOBAL
5606 (CONS (CONS 'F-GET-GLOBAL
5612 (STATE-GLOBAL-LET*-GET-GLOBALS (CDR BINDINGS)))))
5615 STATE-GLOBAL-LET*-PUT-GLOBALS (BINDINGS)
5627 (CONS 'F-BOUNDP-GLOBAL
5644 (CONS 'STATE-GLOBAL-LET* 'NIL))
5654 (CONS 'F-PUT-GLOBAL
5659 (CONS (CONS 'STATE-GLOBAL-LET*-CLEANUP-LST
5663 (STATE-GLOBAL-LET*-PUT-GLOBALS (CDR BINDINGS)))))
5666 STATE-GLOBAL-LET*-CLEANUP
5683 (ALWAYS-BOUNDP-GLOBAL (CAR (CAR BINDINGS)))
5684 (CONS 'F-PUT-GLOBAL
5699 'F-PUT-GLOBAL
5707 (CONS (CONS 'MAKUNBOUND-GLOBAL
5712 (STATE-GLOBAL-LET*-CLEANUP (CDR BINDINGS)
5714 'STATE-GLOBAL-LET*-CLEANUP-LST
6140 (PUT-GLOBAL 'PRINT-CASE CASE STATE)))
6155 (PUT-GLOBAL 'PRINT-BASE BASE STATE)))
6157 (DEFUN SET-PRINT-CIRCLE (X STATE) (PUT-GLOBAL 'PRINT-CIRCLE X STATE))
6159 (DEFUN SET-PRINT-ESCAPE (X STATE) (PUT-GLOBAL 'PRINT-ESCAPE X STATE))
6161 (DEFUN SET-PRINT-PRETTY (X STATE) (PUT-GLOBAL 'PRINT-PRETTY X STATE))
6163 (DEFUN SET-PRINT-RADIX (X STATE) (PUT-GLOBAL 'PRINT-RADIX X STATE))
6165 (DEFUN SET-PRINT-READABLY (X STATE) (PUT-GLOBAL 'PRINT-READABLY X STATE))
6185 (PUT-GLOBAL 'PRINT-LENGTH N STATE)))
6189 (PUT-GLOBAL 'PRINT-LEVEL N STATE)))
6193 (PUT-GLOBAL 'PRINT-LINES N STATE)))
6197 (PUT-GLOBAL 'PRINT-RIGHT-MARGIN
6212 (GLOBAL-TABLE STATE-STATE)))
6219 (GLOBAL-TABLE STATE-STATE)))))
6386 (STATE-GLOBAL-LET*-CLEANUP-LST FILE-NAME TYP STATE)
6388 (MV STATE-GLOBAL-LET*-CLEANUP-LST)
6390 STATE STATE-GLOBAL-LET*-CLEANUP-LST)
6398 (PUT-GLOBAL 'WRITES-OKP
6399 (CAR (NTH '0 STATE-GLOBAL-LET*-CLEANUP-LST))
6409 (PUT-GLOBAL 'WRITES-OKP
6410 (CAR (NTH '0 STATE-GLOBAL-LET*-CLEANUP-LST))
6417 STATE-GLOBAL-LET*-CLEANUP-LST))
6426 (PUT-GLOBAL 'WRITES-OKP 'T STATE)
6428 STATE-GLOBAL-LET*-CLEANUP-LST))
6429 (CONS (CONS (GET-GLOBAL 'WRITES-OKP STATE)
6640 (IF (IF (GET-GLOBAL 'PRINT-ESCAPE STATE)
6641 (GET-GLOBAL 'PRINT-ESCAPE STATE)
6642 (GET-GLOBAL 'PRINT-READABLY STATE))
6643 (MAY-NEED-SLASHES-FN X (GET-GLOBAL 'PRINT-BASE STATE))
6672 (DEFUN OS (WRLD) (GLOBAL-VAL 'OPERATING-SYSTEM WRLD))
6684 (DEFUN W (STATE) (GET-GLOBAL 'CURRENT-ACL2-WORLD STATE))
6848 (PUT-GLOBAL 'MAIN-TIMER
6851 (IF (IF (BOUNDP-GLOBAL 'MAIN-TIMER STATE)
6852 (RATIONALP (GET-GLOBAL 'MAIN-TIMER STATE))
6854 (GET-GLOBAL 'MAIN-TIMER STATE)
6886 (PUT-GLOBAL 'TIMER-ALIST
6888 VAL (GET-GLOBAL 'TIMER-ALIST STATE))
6892 (CDR (ASSOC-EQ NAME (GET-GLOBAL 'TIMER-ALIST STATE))))
7087 (GET-GLOBAL 'CURRENT-PACKAGE STATE))
7089 (GET-GLOBAL 'CURRENT-PACKAGE STATE))
7092 (CAR (CDR (ASSOC-EQUAL (GET-GLOBAL 'CURRENT-PACKAGE STATE)
7093 (GLOBAL-VAL 'KNOWN-PACKAGE-ALIST
7094 (GET-GLOBAL 'CURRENT-ACL2-WORLD
7109 (IF (EQ (GET-GLOBAL 'PRINT-CASE STATE)
7119 (DEFUN CURRENT-PACKAGE (STATE) (GET-GLOBAL 'CURRENT-PACKAGE STATE))
7123 'GLOBAL-VALUE
7132 'GLOBAL-VALUE
7159 (DEFUN LD-SKIP-PROOFSP (STATE) (GET-GLOBAL 'LD-SKIP-PROOFSP STATE))
7199 (GLOBAL-VAL 'FREE-VAR-RUNES-ONCE WRLD)
7200 (GLOBAL-VAL 'FREE-VAR-RUNES-ALL WRLD)))
7317 (GET-GLOBAL 'CERTIFY-BOOK-INFO STATE)
7325 (PUT-GLOBAL 'COMPILER-ENABLED