/seL4-l4v-10.1.1/isabelle/Admin/lib/Tools/ |
H A D | makedist_bundle | 63 for ENTRY in "${CLASSPATH_ENTRIES[@]}" 65 ENTRY=$(echo "$ENTRY" | perl -n -e " 71 DISTRIBITION_CLASSPATH["${#DISTRIBITION_CLASSPATH[@]}"]="$ENTRY" 77 for ENTRY in "${DISTRIBITION_CLASSPATH[@]}" 79 echo " $ENTRY" 206 for ENTRY in "${DISTRIBITION_CLASSPATH[@]}" 209 LINUX_CLASSPATH="\\\$ISABELLE_HOME/$ENTRY" 211 LINUX_CLASSPATH="$LINUX_CLASSPATH:\\\$ISABELLE_HOME/$ENTRY" 263 for ENTRY i [all...] |
/seL4-l4v-10.1.1/l4v/isabelle/Admin/lib/Tools/ |
H A D | makedist_bundle | 63 for ENTRY in "${CLASSPATH_ENTRIES[@]}" 65 ENTRY=$(echo "$ENTRY" | perl -n -e " 71 DISTRIBITION_CLASSPATH["${#DISTRIBITION_CLASSPATH[@]}"]="$ENTRY" 77 for ENTRY in "${DISTRIBITION_CLASSPATH[@]}" 79 echo " $ENTRY" 206 for ENTRY in "${DISTRIBITION_CLASSPATH[@]}" 209 LINUX_CLASSPATH="\\\$ISABELLE_HOME/$ENTRY" 211 LINUX_CLASSPATH="$LINUX_CLASSPATH:\\\$ISABELLE_HOME/$ENTRY" 263 for ENTRY i [all...] |
/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/libffi/src/arc/ |
H A D | arcompact.S | 33 #define ENTRY(x) .globl CNAME(x)` .type CNAME(x),%function` CNAME(x): define 44 ENTRY(ffi_call_ARCompact) 107 ENTRY(ffi_closure_ARCompact)
|
/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/libffi/src/m32r/ |
H A D | sysv.S | 34 #define ENTRY(x) .globl CNAME(x)! .type CNAME(x),%function! CNAME(x): define 47 ENTRY(ffi_call_SYSV)
|
/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/libffi/src/xtensa/ |
H A D | sysv.S | 31 #define ENTRY(name) .text; .globl name; .type name,@function; .align 4; name: define 56 ENTRY(ffi_call_SYSV) 168 ENTRY(ffi_cacheflush) 183 ENTRY(ffi_trampoline) 202 ENTRY(ffi_closure_SYSV)
|
/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/libffi/src/powerpc/ |
H A D | asm.h | 77 #define ENTRY(name) \ macro 93 /* EALIGN is like ENTRY, but does alignment to 'words'*4 bytes
|
H A D | sysv.S | 35 ENTRY(ffi_call_SYSV)
|
H A D | ppc_closure.S | 36 ENTRY(ffi_closure_SYSV)
|
/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/libffi/src/arm/ |
H A D | sysv.S | 44 #define ENTRY(x) .globl _##x; _##x: define 46 #define ENTRY(x) .globl CNAME(x); .type CNAME(x),%function; CNAME(x): define 120 ENTRY(name); \ 131 ENTRY(name); \ 484 ENTRY(ffi_arm_trampoline)
|
/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/libffi/src/metag/ |
H A D | sysv.S | 43 #define ENTRY(x) .globl CNAME(x); .type CNAME(x), %function; CNAME(x): define 83 ENTRY(\name) 302 ENTRY(ffi_metag_trampoline)
|
/seL4-l4v-10.1.1/HOL4/src/quotient/src/ |
H A D | quotient.sig | 356 (* MAIN ENTRY POINT: *) 375 (* ALTERNATE ENTRY POINT: *) 394 (* MAIN ENTRY POINT INCLUDING STANDARD THEOREMS: *) 413 (* ALTERNATE ENTRY POINT INCLUDING STANDARD THEOREMS: *) 432 (* MAIN ENTRY POINT WITH JUST STANDARD THEOREMS: *) 448 (* ALTERNATE ENTRY POINT WITH JUST STANDARD THEOREMS: *) 473 (* MAIN ENTRY POINT FOR SUBSET TYPE: *)
|
H A D | quotient.sml | 3771 (* ALTERNATIVE ENTRY POINT. *) 3831 (* MAIN ENTRY POINT. *) 4165 (* MAIN ENTRY POINT FOR SUBSET TYPES. *)
|
/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/libffi/src/pa/ |
H A D | hpux32.S | 47 .export ffi_call_pa32,ENTRY,PRIV_LEV=3 266 .export ffi_closure_pa32,ENTRY,PRIV_LEV=3,RTNVAL=GR
|
/seL4-l4v-10.1.1/isabelle/src/Tools/jEdit/src/ |
H A D | jedit_bibtex.scala | 64 case Bibtex.Token.Kind.ENTRY => JEditToken.KEYWORD1
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/jEdit/src/ |
H A D | jedit_bibtex.scala | 64 case Bibtex.Token.Kind.ENTRY => JEditToken.KEYWORD1
|
/seL4-l4v-10.1.1/isabelle/src/Pure/Thy/ |
H A D | bibtex.scala | 321 val ENTRY = Value("entry") 337 kind == Token.Kind.ENTRY || 517 else if (is_entry(a)) Token.Kind.ENTRY
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Pure/Thy/ |
H A D | bibtex.scala | 321 val ENTRY = Value("entry") 337 kind == Token.Kind.ENTRY || 517 else if (is_entry(a)) Token.Kind.ENTRY
|
/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/libffi/src/sh/ |
H A D | sysv.S | 35 #define ENTRY(x) .globl CNAME(x); .type CNAME(x),%function; CNAME(x): define 54 ENTRY(ffi_call_SYSV) 497 ENTRY(ffi_closure_SYSV)
|
/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/libffi/src/sh64/ |
H A D | sysv.S | 36 #define ENTRY(x) .globl CNAME(x); .type CNAME(x),%function; CNAME(x): define 57 ENTRY(ffi_call_SYSV) 323 ENTRY(ffi_closure_SYSV)
|
/seL4-l4v-10.1.1/HOL4/examples/acl2/ml/ |
H A D | defaxioms.lisp.trans.ml | 5084 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "BIG-CLOCK-ENTRY") ( 5093 "UPDATE-BIG-CLOCK-ENTRY") (mkpair (mkpair (mksym "ACL2" "X") (mkpair (mksym 5884 "COMMON-LISP" "INTEGERP") (mkpair (mkpair (mksym "ACL2" "BIG-CLOCK-ENTRY") ( 7001 mkpair (mksym "COMMON-LISP" "LAMBDA") (mkpair (mkpair (mksym "ACL2" "ENTRY") ( 7007 mksym "ACL2" "ENTRY") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym 7009 "COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "ENTRY") (mksym "COMMON-LISP" 7026 mkpair (mksym "COMMON-LISP" "LAMBDA") (mkpair (mkpair (mksym "ACL2" "ENTRY") ( 7032 mksym "ACL2" "ENTRY") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym 7034 "COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "ENTRY") (mksym "COMMON-LISP" 7172 "LAMBDA") (mkpair (mkpair (mksym "ACL2" "ENTRY") (mkpai [all...] |
/seL4-l4v-10.1.1/HOL4/examples/acl2/tests/round-trip/gold/ |
H A D | axioms.sml | 8810 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "BIG-CLOCK-ENTRY") ( 8819 "UPDATE-BIG-CLOCK-ENTRY") (mkpair (mkpair (mksym "ACL2" "X") (mkpair (mksym 9936 mkpair (mksym "ACL2" "DMR-START") (mkpair (mksym "ACL2" "REWRITE-ENTRY") ( 10184 "COMMON-LISP" "INTEGERP") (mkpair (mkpair (mksym "ACL2" "BIG-CLOCK-ENTRY") ( 10489 mkpair (mksym "ACL2" "DMR-START") (mkpair (mksym "ACL2" "REWRITE-ENTRY") ( 11072 mkpair (mksym "ACL2" "DMR-START") (mkpair (mksym "ACL2" "REWRITE-ENTRY") ( 11650 mkpair (mksym "ACL2" "DMR-START") (mkpair (mksym "ACL2" "REWRITE-ENTRY") ( 12060 mkpair (mksym "ACL2" "DMR-START") (mkpair (mksym "ACL2" "REWRITE-ENTRY") ( 13979 mksym "COMMON-LISP" "LAMBDA") (mkpair (mkpair (mksym "ACL2" "ENTRY") (mkpair ( 13984 mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "ENTRY") ( [all...] |
/seL4-l4v-10.1.1/HOL4/examples/acl2/examples/M1/ |
H A D | axioms.ml | 8810 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "BIG-CLOCK-ENTRY") ( 8819 "UPDATE-BIG-CLOCK-ENTRY") (mkpair (mkpair (mksym "ACL2" "X") (mkpair (mksym 9936 mkpair (mksym "ACL2" "DMR-START") (mkpair (mksym "ACL2" "REWRITE-ENTRY") ( 10184 "COMMON-LISP" "INTEGERP") (mkpair (mkpair (mksym "ACL2" "BIG-CLOCK-ENTRY") ( 10489 mkpair (mksym "ACL2" "DMR-START") (mkpair (mksym "ACL2" "REWRITE-ENTRY") ( 11072 mkpair (mksym "ACL2" "DMR-START") (mkpair (mksym "ACL2" "REWRITE-ENTRY") ( 11650 mkpair (mksym "ACL2" "DMR-START") (mkpair (mksym "ACL2" "REWRITE-ENTRY") ( 12060 mkpair (mksym "ACL2" "DMR-START") (mkpair (mksym "ACL2" "REWRITE-ENTRY") ( 13979 mksym "COMMON-LISP" "LAMBDA") (mkpair (mkpair (mksym "ACL2" "ENTRY") (mkpair ( 13984 mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "ENTRY") ( [all...] |
H A D | PKGS.sml | 1222 ("BIG-CLOCK-ENTRY" , "ACL2-USER" , "ACL2"), 2775 ("UPDATE-BIG-CLOCK-ENTRY" , "ACL2-USER" , "ACL2"), 3135 ("BIG-CLOCK-ENTRY" , "U" , "ACL2"), 4678 ("UPDATE-BIG-CLOCK-ENTRY" , "U" , "ACL2"), 4971 ("BIG-CLOCK-ENTRY" , "ACL2-ASG" , "ACL2"), 6524 ("UPDATE-BIG-CLOCK-ENTRY" , "ACL2-ASG" , "ACL2"), 6820 ("BIG-CLOCK-ENTRY" , "ACL2-AGP" , "ACL2"), 8373 ("UPDATE-BIG-CLOCK-ENTRY" , "ACL2-AGP" , "ACL2"), 8669 ("BIG-CLOCK-ENTRY" , "ACL2-CRG" , "ACL2"), 10222 ("UPDATE-BIG-CLOCK-ENTRY" , "ACL [all...] |
H A D | hol_defaxiomsScript.sml | 2918 [oracles: DEFUN ACL2::BIG-CLOCK-ENTRY, DISK_THM] [axioms: ] [] 2923 [oracles: DEFUN ACL2::UPDATE-BIG-CLOCK-ENTRY, DISK_THM] [axioms: ] []
|
/seL4-l4v-10.1.1/HOL4/examples/acl2/tests/inputs/ |
H A D | PKGS.sml | 1181 ("BIG-CLOCK-ENTRY" , "ACL2-USER" , "ACL2"), 2734 ("UPDATE-BIG-CLOCK-ENTRY" , "ACL2-USER" , "ACL2"), 3094 ("BIG-CLOCK-ENTRY" , "U" , "ACL2"), 4637 ("UPDATE-BIG-CLOCK-ENTRY" , "U" , "ACL2"), 4930 ("BIG-CLOCK-ENTRY" , "ACL2-ASG" , "ACL2"), 6483 ("UPDATE-BIG-CLOCK-ENTRY" , "ACL2-ASG" , "ACL2"), 6779 ("BIG-CLOCK-ENTRY" , "ACL2-AGP" , "ACL2"), 8332 ("UPDATE-BIG-CLOCK-ENTRY" , "ACL2-AGP" , "ACL2"), 8628 ("BIG-CLOCK-ENTRY" , "ACL2-CRG" , "ACL2"), 10181 ("UPDATE-BIG-CLOCK-ENTRY" , "ACL [all...] |