/seL4-l4v-10.1.1/HOL4/examples/CCS/ |
H A D | ObsCongrLawsScript.sml | 87 OBS_CONGR (par (prefix u E) (prefix tau E')) 88 (sum (prefix u (par E (prefix tau E'))) 89 (prefix tau (par (prefix u E) E'))) 97 OBS_CONGR (par (prefix tau E) (prefix u E')) 98 (sum (prefix tau (par E (prefix [all...] |
H A D | WeakLawsScript.sml | 105 WEAK_EQUIV (par (prefix u E) (prefix tau E')) 106 (sum (prefix u (par E (prefix tau E'))) 107 (prefix tau (par (prefix u E) E'))) 115 WEAK_EQUIV (par (prefix tau E) (prefix u E')) 116 (sum (prefix tau (par E (prefix [all...] |
H A D | StrongLawsScript.sml | 522 STRONG_EQUIV (par (prefix u E) (prefix tau E')) 523 (sum (prefix u (par E (prefix tau E'))) 524 (prefix tau (par (prefix u E) E')))``, 529 (?(u' :'b Action) E1 E2. (x = par (prefix u' E1) (prefix tau E2)) /\ 530 (y = sum (prefix u' (par E1 (prefix ta [all...] |
H A D | CongruenceScript.sml | 49 (!a c. OH_CONTEXT c ==> OH_CONTEXT (\t. prefix a (c t))) /\ (* OH_CONTEXT2 *) 86 (!a e. CONTEXT e ==> CONTEXT (\t. prefix a (e t))) /\ (* CONTEXT3 *) 102 ``!a :'b Action. CONTEXT (\t. prefix a t)``, 204 (!a e. GCONTEXT e ==> GCONTEXT (\t. prefix a (e t))) /\ (* GCONTEXT3 *) 207 ==> GCONTEXT (\t. sum (prefix a1 (e1 t)) (* GCONTEXT4 *) 208 (prefix a2 (e2 t)))) /\ 223 ``!a :'b Action. GCONTEXT (\t. prefix a t)``, 257 Know `CONTEXT (\t. (prefix a1 (e1 t)))` 259 Know `CONTEXT (\t. (prefix a2 (e2 t)))` 263 Know `CONTEXT (\t. (\t. (prefix a [all...] |
H A D | CoarsestCongrScript.sml | 27 |- !E E'. OBS_CONGR (sum E (prefix tau (sum E' E))) (prefix tau (sum E' E)) 31 ``!E E'. OBS_CONGR (sum E (prefix tau (sum E' E))) (prefix tau (sum E' E))``, 89 ``!p q. (OBS_CONGR p q \/ OBS_CONGR p (prefix tau q) \/ 90 OBS_CONGR (prefix tau p) q) ==> WEAK_EQUIV p q``, 107 ``!p q. WEAK_EQUIV p q ==> (OBS_CONGR p q \/ OBS_CONGR p (prefix tau q) 108 \/ OBS_CONGR (prefix tau p) q)``, 122 take [`prefix tau q`, `q`] \\ 150 take [`prefix ta [all...] |
H A D | ObsCongrConv.sml | 172 |- !u E. OBS_CONGR (prefix u (prefix tau E)) (prefix u E) *) 192 |- !E. OBS_CONGR (sum E (prefix tau E)) (prefix tau E) 211 OBS_CONGR (sum (prefix u (sum E (prefix tau E'))) (prefix u E')) 212 (prefix u (sum E (prefix ta [all...] |
/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/libffi/ |
H A D | generate-ios-source-and-headers.py | 49 prefix = "#if !defined(__arm__) && defined(__i386__)\n\n" variable in class:simulator_platform 59 prefix = "#ifdef __arm__\n\n" variable in class:device_platform 63 def move_file(src_dir, dst_dir, filename, file_suffix=None, prefix='', suffix=''): 75 if prefix: 76 out_file.write(prefix) 85 def move_source_tree(src_dir, dest_dir, dest_include_dir, arch=None, prefix=None, suffix=None): 89 def move_dir(arch, prefix='', suffix='', files=[]): 97 move_file(root, dest_include_dir, file, arch, prefix=prefix, suffix=suffix) 101 move_file(root, outroot, file, prefix [all...] |
H A D | generate-osx-source-and-headers.py | 44 prefix = "#if defined(__i386__) && !defined(__x86_64__)\n\n" variable in class:desktop_platform_32 54 prefix = "#if !defined(__i386__) && defined(__x86_64__)\n\n" variable in class:desktop_platform_64 57 def move_file(src_dir, dst_dir, filename, file_suffix=None, prefix='', suffix=''): 69 if prefix: 70 out_file.write(prefix) 79 def move_source_tree(src_dir, dest_dir, dest_include_dir, arch=None, prefix=None, suffix=None): 83 def move_dir(arch, prefix='', suffix='', files=[]): 91 move_file(root, dest_include_dir, file, arch, prefix=prefix, suffix=suffix) 95 move_file(root, outroot, file, prefix [all...] |
H A D | install-sh | 380 /*) prefix='/';; 381 [-=\(\)!]*) prefix='./';; 382 *) prefix='';; 399 prefix=$prefix$d 400 if test -d "$prefix"; then 407 test -d "$prefix" || exit 1 409 case $prefix in 410 *\'*) qprefix=`echo "$prefix" | sed "s/'/'\\\\\\\\''/g"`;; 411 *) qprefix=$prefix;; [all...] |
/seL4-l4v-10.1.1/graph-refine/graph-to-graph/ |
H A D | graph_to_graph.py | 75 prefix = dir_name + '/' + entry_point_function 76 tcfg_map_file_name = prefix + ".imm.map" 77 current_ilp = prefix + ".imm.ilp" 80 ilp_to_generate = prefix + "_annotated.imm.ilp" 81 sol_to_generate = prefix + "_annotated.imm.sol"
|
/seL4-l4v-10.1.1/HOL4/developers/ |
H A D | genUseScript.sml | 104 type config = {dohelp : bool, prefix : string, prelude : string, 107 val default_config = {dohelp = false, prefix = "", prelude = "", suffix = ""} 115 fun turnOnHelp _ = {dohelp = true, prefix = "", prelude = "", suffix = ""} 116 fun turnOnHOL {dohelp,...} = {dohelp = dohelp, prefix = "use \"", 119 fun setPrefix s {prefix,dohelp,suffix,prelude} = 120 {prefix = s, dohelp = dohelp, suffix = suffix, prelude = prelude} 121 fun setSuffix s {prefix,dohelp,suffix,prelude} = 122 {prefix = prefix, dohelp = dohelp, suffix = s, prelude = prelude} 133 {short = "p", long = ["prefix"], [all...] |
H A D | install-poly.sh | 28 echo "*** Configuring PolyML for prefix: ${PREFIX}" 29 ./configure --prefix=$PREFIX
|
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/common/ |
H A D | temporal_stateScript.sml | 150 `!x (prefix: 'a word list) (postfix: 'a word list) p c q m i a l1 l2. 153 TEMPORAL_NEXT x (p * SEP_ARRAY m i (a - n2w (LENGTH prefix) * i) 154 (prefix ++ l1 ++ postfix)) c 155 (q * SEP_ARRAY m i (a - n2w (LENGTH prefix) * i) 156 (prefix ++ l2 ++ postfix))`, 163 (a - n2w (LENGTH prefix) * i) (prefix: 'a word list)``) 168 (a - n2w (LENGTH (prefix: 'a word list)) * i + 169 n2w (LENGTH (prefix ++ l1)) * i)
|
/seL4-l4v-10.1.1/HOL4/src/tactictoe/src/ |
H A D | tttNumber.sml | 67 fun prefix l1 l2 = case (l1,l2) of function 69 | (_,[]) => raise ERR "prefix" "" 72 then prefix m1 m2 73 else raise ERR "prefix" "" 79 let val r = prefix l1 l2 in lrep @ r end
|
/seL4-l4v-10.1.1/seL4/manual/tools/ |
H A D | gen_invocations.py | 48 prefix = FN_DECL_PREFIX 57 return "%s\n%s %s %s(%s);" % (comment, prefix, return_type, name, param_list) 72 # figure out the prefix to use for an interface group id. This makes groups per arch, 74 prefix = None 79 (path, prefix) = os.path.split(path) 83 group_id = interface_name if prefix is None else prefix + '_' + interface_name
|
/seL4-l4v-10.1.1/HOL4/polyml/ |
H A D | install-sh | 380 /*) prefix='/';; 381 [-=\(\)!]*) prefix='./';; 382 *) prefix='';; 399 prefix=$prefix$d 400 if test -d "$prefix"; then 407 test -d "$prefix" || exit 1 409 case $prefix in 410 *\'*) qprefix=`echo "$prefix" | sed "s/'/'\\\\\\\\''/g"`;; 411 *) qprefix=$prefix;; [all...] |
/seL4-l4v-10.1.1/l4v/spec/haskell/ |
H A D | mkhsboot.pl | 15 $prefix = $literate ? "> " : ""; 35 $imports =~ s/\s+/\n${prefix}import /g; 45 print "${prefix}-- this file is automatically generated, do not edit\n"; 46 print "${prefix}module $modname($explist) where\n${prefix}import Prelude hiding(Word)\n$imports\n\n";
|
/seL4-l4v-10.1.1/HOL4/src/HolQbf/ |
H A D | QbfConv.sig | 33 (* [last_quant_conv c] strips a quantifier (! and ? only) prefix down 37 (* applies a conversion under a quantifier prefix of foralls and exists *) 40 (* [last_quant_seq_conv cq cb] applies cb under the quantifier prefix and 46 (* applies cb under the quantifier prefix, and then, if the innermost
|
/seL4-l4v-10.1.1/HOL4/src/portableML/ |
H A D | UTF8Set.sig | 33 prefix of s that is also a member of t, and rest is the rest of the string 34 s. If there is no prefix of s in t, then the function returns NONE.
|
/seL4-l4v-10.1.1/isabelle/src/Tools/Metis/src/ |
H A D | Name.sml | 30 val prefix = "_"; value 32 fun numName i = mkPrefix prefix (Int.toString i);
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/Metis/src/ |
H A D | Name.sml | 30 val prefix = "_"; value 32 fun numName i = mkPrefix prefix (Int.toString i);
|
/seL4-l4v-10.1.1/HOL4/doc/hol-mode/ |
H A D | hol-mode.tex | 11 All of these commands are executed by first typing the HOL prefix 28 \emph{prefix argument}, moves back that many tactics. 30 next tactic in the source text in the current buffer. With a \emph{prefix 43 \emph{prefix argument}, or if in transient mark mode with an active 49 \emph{prefix argument}), prompts for the name of the library. 52 With a \emph{prefix argument} also drops the goal. 55 numeric \emph{prefix argument} rotates that many out of the way,
|
/seL4-l4v-10.1.1/graph-refine/scripts/ |
H A D | setup-HOL4.sh | 44 (./configure --prefix=$POLY_DIR/deploy) &> $OUT
|
/seL4-l4v-10.1.1/isabelle/src/Pure/PIDE/ |
H A D | line.scala | 192 val (prefix, lines1) = lines.splitAt(l1) 198 if (lines1.isEmpty) ("", prefix ::: Document.split(insert)) 202 (removed_text, prefix ::: Document.split(changed_text) ::: rest1) 212 if (lines1.isEmpty) ("", prefix ::: Document.split(insert)) 220 (removed_text, prefix ::: Document.split(changed_text) ::: rest2)
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Pure/PIDE/ |
H A D | line.scala | 192 val (prefix, lines1) = lines.splitAt(l1) 198 if (lines1.isEmpty) ("", prefix ::: Document.split(insert)) 202 (removed_text, prefix ::: Document.split(changed_text) ::: rest1) 212 if (lines1.isEmpty) ("", prefix ::: Document.split(insert)) 220 (removed_text, prefix ::: Document.split(changed_text) ::: rest2)
|