/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/ |
H A D | x86assembly_gas32.S | 52 #define GLOBAL .globl define 54 #define GLOBAL .global define 58 GLOBAL EXTNAME(id); \ label
|
H A D | x86assembly_gas64.S | 61 #define GLOBAL .globl define 63 #define GLOBAL .global define 67 GLOBAL EXTNAME(id); \ label
|
/seL4-l4v-10.1.1/HOL4/examples/separationLogic/src/holfoot/ |
H A D | holfoot.lex | 33 ("global", GLOBAL),
|
/seL4-l4v-10.1.1/HOL4/examples/acl2/examples/M1/ |
H A D | hol_defaxiomsScript.sml | 2540 [oracles: DEFUN ACL2::GLOBAL-VAL, DISK_THM] [axioms: ] [] 2542 fgetprop var (asym "GLOBAL-VALUE") 2546 "GLOBAL-VAL didn't find a value. Initialize this ~\n symbol in PRIMORDIAL-WORLD-GLOBALS."]) 2888 [oracles: DEFUN ACL2::GLOBAL-TABLE, DISK_THM] [axioms: ] [] 2893 [oracles: DEFUN ACL2::UPDATE-GLOBAL-TABLE, DISK_THM] [axioms: ] [] 3258 (fgetprop (asym "KNOWN-PACKAGE-ALIST") (asym "GLOBAL-VALUE") nil 3376 [oracles: DEFUN ACL2::GLOBAL-TABLE-CARS1] [axioms: ] [] 3382 [oracles: DEFUN ACL2::GLOBAL-TABLE-CARS] [axioms: ] [] 3393 [oracles: DEFUN ACL2::BOUNDP-GLOBAL] [axioms: ] [] 3405 [oracles: DEFUN ACL2::MAKUNBOUND-GLOBAL] [axiom [all...] |
H A D | PKGS.sml | 1276 ("BOUNDP-GLOBAL" , "ACL2-USER" , "ACL2"), 1747 ("GET-GLOBAL" , "ACL2-USER" , "ACL2"), 1762 ("GLOBAL-TABLE" , "ACL2-USER" , "ACL2"), 1763 ("GLOBAL-TABLE-CARS" , "ACL2-USER" , "ACL2"), 1764 ("GLOBAL-TABLE-CARS1" , "ACL2-USER" , "ACL2"), 1765 ("GLOBAL-VAL" , "ACL2-USER" , "ACL2"), 2011 ("MAKUNBOUND-GLOBAL" , "ACL2-USER" , "ACL2"), 2300 ("PUT-GLOBAL" , "ACL2-USER" , "ACL2"), 2579 ("STATE-GLOBAL-LET*-CLEANUP" , "ACL2-USER" , "ACL2"), 2580 ("STATE-GLOBAL [all...] |
H A D | axioms.ml | 4224 "COMMON-LISP" "QUOTE") (mkpair (mksym "ACL2" "F-GET-GLOBAL") (mksym 4256 "STATE-GLOBAL-LET*") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym 7056 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "GLOBAL-VAL") ( 7060 mksym "ACL2" "GLOBAL-VALUE") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair ( 8760 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "GLOBAL-TABLE") ( 8769 "UPDATE-GLOBAL-TABLE") (mkpair (mkpair (mksym "ACL2" "X") (mkpair (mksym 9726 "ACL2" "GLOBAL-TABLE") (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) ( 9767 "ACL2" "GLOBAL-ENABLED-STRUCTURE") (mksym "COMMON-LISP" "NIL")) (mkpair ( 9823 "PUT-GLOBAL") (mkpair (mksym "ACL2" "CLOSE-INPUT-CHANNEL") (mkpair (mksym 9824 "ACL2" "MAKUNBOUND-GLOBAL") (mkpai [all...] |
/seL4-l4v-10.1.1/HOL4/examples/acl2/examples/acl2-hol-ltl-paper-example/ |
H A D | hol_defaxiomsScript.sml | 2502 [oracles: DEFUN ACL2::GLOBAL-VAL, DISK_THM] [axioms: ] [] 2504 fgetprop var (asym "GLOBAL-VALUE") 2508 "GLOBAL-VAL didn't find a value. Initialize this ~\n symbol in PRIMORDIAL-WORLD-GLOBALS."]) 2850 [oracles: DEFUN ACL2::GLOBAL-TABLE, DISK_THM] [axioms: ] [] 2855 [oracles: DEFUN ACL2::UPDATE-GLOBAL-TABLE, DISK_THM] [axioms: ] [] 3220 (fgetprop (asym "KNOWN-PACKAGE-ALIST") (asym "GLOBAL-VALUE") nil 3338 [oracles: DEFUN ACL2::GLOBAL-TABLE-CARS1] [axioms: ] [] 3344 [oracles: DEFUN ACL2::GLOBAL-TABLE-CARS] [axioms: ] [] 3355 [oracles: DEFUN ACL2::BOUNDP-GLOBAL] [axioms: ] [] 3367 [oracles: DEFUN ACL2::MAKUNBOUND-GLOBAL] [axiom [all...] |
H A D | acl2_packageScript.sml | 212 ("BOUNDP-GLOBAL", "ACL2-USER", "ACL2"), 404 ("GET-GLOBAL", "ACL2-USER", "ACL2"), 409 ("GLOBAL-TABLE", "ACL2-USER", "ACL2"), 410 ("GLOBAL-TABLE-CARS", "ACL2-USER", "ACL2"), 411 ("GLOBAL-TABLE-CARS1", "ACL2-USER", "ACL2"), 412 ("GLOBAL-VAL", "ACL2-USER", "ACL2"), 509 ("MAKUNBOUND-GLOBAL", "ACL2-USER", "ACL2"), 631 ("PUT-GLOBAL", "ACL2-USER", "ACL2"), 728 ("STATE-GLOBAL-LET*-CLEANUP", "ACL2-USER", "ACL2"), 729 ("STATE-GLOBAL [all...] |
/seL4-l4v-10.1.1/HOL4/examples/acl2/ml/ |
H A D | hol_defaxiomsScript.sml | 2498 [oracles: DEFUN ACL2::GLOBAL-VAL, DISK_THM] [axioms: ] [] 2500 fgetprop var (asym "GLOBAL-VALUE") 2504 "GLOBAL-VAL didn't find a value. Initialize this ~\n symbol in PRIMORDIAL-WORLD-GLOBALS."]) 2846 [oracles: DEFUN ACL2::GLOBAL-TABLE, DISK_THM] [axioms: ] [] 2851 [oracles: DEFUN ACL2::UPDATE-GLOBAL-TABLE, DISK_THM] [axioms: ] [] 3216 (fgetprop (asym "KNOWN-PACKAGE-ALIST") (asym "GLOBAL-VALUE") nil 3334 [oracles: DEFUN ACL2::GLOBAL-TABLE-CARS1] [axioms: ] [] 3340 [oracles: DEFUN ACL2::GLOBAL-TABLE-CARS] [axioms: ] [] 3351 [oracles: DEFUN ACL2::BOUNDP-GLOBAL] [axioms: ] [] 3363 [oracles: DEFUN ACL2::MAKUNBOUND-GLOBAL] [axiom [all...] |
H A D | kpa-v2-9-3.ml | 101 ("BOUNDP-GLOBAL", "ACL2-USER", "ACL2"), 293 ("GET-GLOBAL", "ACL2-USER", "ACL2"), 298 ("GLOBAL-TABLE", "ACL2-USER", "ACL2"), 299 ("GLOBAL-TABLE-CARS", "ACL2-USER", "ACL2"), 300 ("GLOBAL-TABLE-CARS1", "ACL2-USER", "ACL2"), 301 ("GLOBAL-VAL", "ACL2-USER", "ACL2"), 398 ("MAKUNBOUND-GLOBAL", "ACL2-USER", "ACL2"), 520 ("PUT-GLOBAL", "ACL2-USER", "ACL2"), 617 ("STATE-GLOBAL-LET*-CLEANUP", "ACL2-USER", "ACL2"), 618 ("STATE-GLOBAL [all...] |
H A D | acl2_packageScript.sml | 212 ("BOUNDP-GLOBAL", "ACL2-USER", "ACL2"), 404 ("GET-GLOBAL", "ACL2-USER", "ACL2"), 409 ("GLOBAL-TABLE", "ACL2-USER", "ACL2"), 410 ("GLOBAL-TABLE-CARS", "ACL2-USER", "ACL2"), 411 ("GLOBAL-TABLE-CARS1", "ACL2-USER", "ACL2"), 412 ("GLOBAL-VAL", "ACL2-USER", "ACL2"), 509 ("MAKUNBOUND-GLOBAL", "ACL2-USER", "ACL2"), 631 ("PUT-GLOBAL", "ACL2-USER", "ACL2"), 728 ("STATE-GLOBAL-LET*-CLEANUP", "ACL2-USER", "ACL2"), 729 ("STATE-GLOBAL [all...] |
H A D | defaxioms.lisp.trans.ml | 4121 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "GLOBAL-VAL") ( 4125 mksym "ACL2" "GLOBAL-VALUE") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair ( 5034 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "GLOBAL-TABLE") ( 5043 "UPDATE-GLOBAL-TABLE") (mkpair (mkpair (mksym "ACL2" "X") (mkpair (mksym 5757 "ACL2" "GLOBAL-TABLE") (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) ( 5837 mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2" "GLOBAL-TABLE") ( 5843 mkpair (mkpair (mksym "ACL2" "GLOBAL-TABLE") (mkpair (mksym "ACL2" "X") ( 5855 "NIL"))) (mkpair (mkpair (mksym "ACL2" "GLOBAL-TABLE") (mkpair (mksym "ACL2" 5862 mkpair (mkpair (mksym "ACL2" "GLOBAL-TABLE") (mkpair (mksym "ACL2" "X") ( 5869 "GLOBAL [all...] |
/seL4-l4v-10.1.1/HOL4/examples/acl2/tests/inputs/ |
H A D | PKGS.sml | 1235 ("BOUNDP-GLOBAL" , "ACL2-USER" , "ACL2"), 1706 ("GET-GLOBAL" , "ACL2-USER" , "ACL2"), 1721 ("GLOBAL-TABLE" , "ACL2-USER" , "ACL2"), 1722 ("GLOBAL-TABLE-CARS" , "ACL2-USER" , "ACL2"), 1723 ("GLOBAL-TABLE-CARS1" , "ACL2-USER" , "ACL2"), 1724 ("GLOBAL-VAL" , "ACL2-USER" , "ACL2"), 1970 ("MAKUNBOUND-GLOBAL" , "ACL2-USER" , "ACL2"), 2259 ("PUT-GLOBAL" , "ACL2-USER" , "ACL2"), 2538 ("STATE-GLOBAL-LET*-CLEANUP" , "ACL2-USER" , "ACL2"), 2539 ("STATE-GLOBAL [all...] |
/seL4-l4v-10.1.1/isabelle/src/Pure/Thy/ |
H A D | sessions.scala | 747 private val GLOBAL = "global" 752 Outer_Syntax.empty + "(" + ")" + "+" + "," + "=" + "[" + "]" + GLOBAL + IN + 798 ($$$("(") ~! $$$(GLOBAL) ~ $$$(")")) ^^ { case _ => true } | success(false)
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Pure/Thy/ |
H A D | sessions.scala | 747 private val GLOBAL = "global" 752 Outer_Syntax.empty + "(" + ")" + "+" + "," + "=" + "[" + "]" + GLOBAL + IN + 798 ($$$("(") ~! $$$(GLOBAL) ~ $$$(")")) ^^ { case _ => true } | success(false)
|
/seL4-l4v-10.1.1/HOL4/examples/acl2/tests/round-trip/gold/ |
H A D | axioms.sml | 4224 "COMMON-LISP" "QUOTE") (mkpair (mksym "ACL2" "F-GET-GLOBAL") (mksym 4256 "STATE-GLOBAL-LET*") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym 7056 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "GLOBAL-VAL") ( 7060 mksym "ACL2" "GLOBAL-VALUE") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair ( 8760 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "GLOBAL-TABLE") ( 8769 "UPDATE-GLOBAL-TABLE") (mkpair (mkpair (mksym "ACL2" "X") (mkpair (mksym 9726 "ACL2" "GLOBAL-TABLE") (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) ( 9767 "ACL2" "GLOBAL-ENABLED-STRUCTURE") (mksym "COMMON-LISP" "NIL")) (mkpair ( 9823 "PUT-GLOBAL") (mkpair (mksym "ACL2" "CLOSE-INPUT-CHANNEL") (mkpair (mksym 9824 "ACL2" "MAKUNBOUND-GLOBAL") (mkpai [all...] |