Searched refs:GLOBAL (Results 1 - 16 of 16) sorted by relevance

/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/
H A Dx86assembly_gas32.S52 #define GLOBAL .globl define
54 #define GLOBAL .global define
58 GLOBAL EXTNAME(id); \ label
H A Dx86assembly_gas64.S61 #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 Dholfoot.lex33 ("global", GLOBAL),
/seL4-l4v-10.1.1/HOL4/examples/acl2/examples/M1/
H A Dhol_defaxiomsScript.sml2540 [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 DPKGS.sml1276 ("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 Daxioms.ml4224 "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 Dhol_defaxiomsScript.sml2502 [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 Dacl2_packageScript.sml212 ("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 Dhol_defaxiomsScript.sml2498 [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 Dkpa-v2-9-3.ml101 ("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 Dacl2_packageScript.sml212 ("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 Ddefaxioms.lisp.trans.ml4121 (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 DPKGS.sml1235 ("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 Dsessions.scala747 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 Dsessions.scala747 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 Daxioms.sml4224 "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...]

Completed in 401 milliseconds