Searched refs:prefix (Results 1 - 25 of 186) sorted by relevance

12345678

/seL4-l4v-10.1.1/HOL4/examples/CCS/
H A DObsCongrLawsScript.sml87 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 DWeakLawsScript.sml105 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 DStrongLawsScript.sml522 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 DCongruenceScript.sml49 (!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 DCoarsestCongrScript.sml27 |- !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 DObsCongrConv.sml172 |- !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 Dgenerate-ios-source-and-headers.py49 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 Dgenerate-osx-source-and-headers.py44 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 Dinstall-sh380 /*) 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 Dgraph_to_graph.py75 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 DgenUseScript.sml104 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 Dinstall-poly.sh28 echo "*** Configuring PolyML for prefix: ${PREFIX}"
29 ./configure --prefix=$PREFIX
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/common/
H A Dtemporal_stateScript.sml150 `!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 DtttNumber.sml67 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 Dgen_invocations.py48 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 Dinstall-sh380 /*) 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 Dmkhsboot.pl15 $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 DQbfConv.sig33 (* [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 DUTF8Set.sig33 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 DName.sml30 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 DName.sml30 val prefix = "_"; value
32 fun numName i = mkPrefix prefix (Int.toString i);
/seL4-l4v-10.1.1/HOL4/doc/hol-mode/
H A Dhol-mode.tex11 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 Dsetup-HOL4.sh44 (./configure --prefix=$POLY_DIR/deploy) &> $OUT
/seL4-l4v-10.1.1/isabelle/src/Pure/PIDE/
H A Dline.scala192 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 Dline.scala192 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)

Completed in 81 milliseconds

12345678