Searched refs:bs (Results 1 - 25 of 84) sorted by relevance

1234

/seL4-l4v-master/isabelle/lib/browser/awtUtilities/
H A DBorder.java13 int bs; field in class:Border
16 return new Insets(bs*3/2,bs*3/2,bs*3/2,bs*3/2);
22 bs=s;
28 int x1[]={0,bs,w-bs,w}, y1[]={0,bs,bs,
[all...]
/seL4-l4v-master/l4v/isabelle/lib/browser/awtUtilities/
H A DBorder.java13 int bs; field in class:Border
16 return new Insets(bs*3/2,bs*3/2,bs*3/2,bs*3/2);
22 bs=s;
28 int x1[]={0,bs,w-bs,w}, y1[]={0,bs,bs,
[all...]
/seL4-l4v-master/HOL4/src/portableML/
H A Dsmpp.sml41 fun bs2b bs = bs = HOLPP.CONSISTENT
43 fun block bs i p (a,ps) =
47 SOME(res, (a1, PrettyBlock(i, bs2b bs, [], List.rev ps1) :: ps))
63 | b::bs => fpp b >> brk >> pr_list fpp brk bs
71 | b::bs => let
72 fun afterb bres = brk >> mappr_list fpp brk bs >- return o cons bres
H A DHOLPP.sml45 fun bs2b bs = bs = CONSISTENT
46 fun block bs i ps = PrettyBlock(i, bs2b bs, [], ps)
H A DAList.sml100 let val (bs, qs) = vals x ps value
101 in (x, a :: bs) :: coal qs end;
/seL4-l4v-master/isabelle/src/Pure/General/
H A Dmulti_map.scala36 val bs = get_list(a)
37 if (bs.contains(b)) this
38 else new Multi_Map(rep + (a -> (b :: bs)))
43 val bs = get_list(a)
44 if (bs.contains(b)) {
45 bs.filterNot(_ == b) match {
58 case (m1, (a, bs)) => (bs :\ m1) { case (b, m2) => m2.insert(a, b) }
72 for ((a, bs) <- rep.iterator; b <- bs
[all...]
H A Dproperties.scala40 def decode(bs: Bytes, xml_cache: Option[XML.Cache] = None): T =
42 val ps = XML.Decode.properties(YXML.parse_body(bs.text))
60 def uncompress(bs: Bytes,
64 if (bs.isEmpty) Nil
67 XML.Decode.list(XML.Decode.properties)(YXML.parse_body(bs.uncompress(cache = cache).text))
/seL4-l4v-master/l4v/isabelle/src/Pure/General/
H A Dmulti_map.scala36 val bs = get_list(a)
37 if (bs.contains(b)) this
38 else new Multi_Map(rep + (a -> (b :: bs)))
43 val bs = get_list(a)
44 if (bs.contains(b)) {
45 bs.filterNot(_ == b) match {
58 case (m1, (a, bs)) => (bs :\ m1) { case (b, m2) => m2.insert(a, b) }
72 for ((a, bs) <- rep.iterator; b <- bs
[all...]
H A Dproperties.scala40 def decode(bs: Bytes, xml_cache: Option[XML.Cache] = None): T =
42 val ps = XML.Decode.properties(YXML.parse_body(bs.text))
60 def uncompress(bs: Bytes,
64 if (bs.isEmpty) Nil
67 XML.Decode.list(XML.Decode.properties)(YXML.parse_body(bs.uncompress(cache = cache).text))
/seL4-l4v-master/HOL4/src/integer/
H A Dint_bitwiseScript.sml40 (num_of_bits (F::bs) = 2 * num_of_bits bs) /\
41 (num_of_bits (T::bs) = 1 + 2 * num_of_bits bs)`;
44 int_of_bits (bs,rest) =
46 int_not (& (num_of_bits (MAP (~) bs)))
47 else & (num_of_bits bs)`;
52 let (bs,r) = bits_bitwise f ([],r1) (bs2,r2) in
53 (f r1 b2 :: bs, r)) /\
55 let (bs,
[all...]
/seL4-l4v-master/HOL4/Manual/Translations/IT/Tutorial/binomial/
H A Dappendix.tex55 (!as bs.
56 REDUCE plus(APPEND as bs) = plus(REDUCE plus as)(REDUCE plus bs))
61 (!a bs. REDUCE plus(MAP(times a)bs) = times a(REDUCE plus bs))
/seL4-l4v-master/HOL4/Manual/Tutorial/binomial/
H A Dappendix.tex55 (!as bs.
56 REDUCE plus(APPEND as bs) = plus(REDUCE plus as)(REDUCE plus bs))
61 (!a bs. REDUCE plus(MAP(times a)bs) = times a(REDUCE plus bs))
/seL4-l4v-master/HOL4/developers/
H A DforTeX.pl16 s/\\/\\bs{}/g;
/seL4-l4v-master/HOL4/examples/machine-code/instruction-set-models/x86_64/
H A Dx64_seq_monadScript.sml216 (let bs = word2bytes 2 (w:word16) in
217 parT_unit_seq (write_mem_seq ii (a+0w) (EL 0 bs))
218 (write_mem_seq ii (a+1w) (EL 1 bs)))`;
221 (let bs = word2bytes 4 (w:word32) in
222 parT_unit_seq (write_mem_seq ii (a+0w) (EL 0 bs))
223 (parT_unit_seq (write_mem_seq ii (a+1w) (EL 1 bs))
224 (parT_unit_seq (write_mem_seq ii (a+2w) (EL 2 bs))
225 (write_mem_seq ii (a+3w) (EL 3 bs)))))`;
228 (let bs = word2bytes 8 (w:word64) in
229 parT_unit_seq (write_mem_seq ii (a+0w) (EL 0 bs))
[all...]
/seL4-l4v-master/HOL4/examples/miller/ho_prover/
H A Dho_basicTools.sml78 | mk_ho_pat bvs (var, b::bs) =
79 mk_comb (mk_ho_pat bvs (var, bs), mk_bv bvs b);
112 fun ho_raw_match (var, bs) (bvs, tm) sub =
114 val var_bvs = map (mk_bv bvs) bs
122 | check_off_bvs bvs tm (b :: bs) =
127 check_off_bvs bvs a bs
130 fun fo_raw_match (var, bs) (bvs, tm) sub =
132 val body = check_off_bvs bvs tm bs
/seL4-l4v-master/isabelle/src/Pure/PIDE/
H A Dmarkup_tree.scala33 case (bs, (r, entry)) =>
34 require(!bs.isDefinedAt(r))
35 bs + (r -> entry)
125 val bs = branches.range(start, stop)
127 case Some(end) if range overlaps end.range => bs + (end.range -> end)
128 case _ => bs
/seL4-l4v-master/l4v/isabelle/src/Pure/PIDE/
H A Dmarkup_tree.scala33 case (bs, (r, entry)) =>
34 require(!bs.isDefinedAt(r))
35 bs + (r -> entry)
125 val bs = branches.range(start, stop)
127 case Some(end) if range overlaps end.range => bs + (end.range -> end)
128 case _ => bs
/seL4-l4v-master/HOL4/Manual/Description/
H A Dmisc.tex992 \newcommand{\holtm}{\texttt{\bs{}HOLtm}}
993 \newcommand{\holty}{\texttt{\bs{}HOLty}}
994 \newcommand{\holthm}{\texttt{\bs{}HOLthm}}
995 \paragraph{Before starting} In order to use the munger, one must ``include'' (use the \texttt{\bs{}usepackage} command) the \texttt{holtexbasic.sty} style-file, which is found in the HOL source directory \texttt{src/TeX}.
1006 \holtm{}[tt]\{P(SUC n) /\bs{} q\}
1011 or something very close to it, appearing in the resulting document.\footnote{The output is a mixture of typewriter font and math-mode characters embedded in a \texttt{\bs{}texttt} block within an \texttt{\bs{}mbox}.}
1029 The output is suited for inclusion in the normal flow of \LaTeX{} (it is an \texttt{\bs{}mbox}).
1036 Again, the output is wrapped in an \texttt{\bs{}mbox}.
1040 escaped by preceding it with a backslash~(\bs)
[all...]
/seL4-l4v-master/HOL4/examples/theorem-prover/lisp-runtime/implementation/
H A Dlisp_bytecode_stepScript.sml512 ``!bs bc n. code_ptr bc + code_length bs <= n ==>
513 (code_mem (WRITE_CODE bc bs) n = code_mem bc n)``,
524 ``!bs. (code_mem (WRITE_CODE (BC_CODE ((\x. NONE),0)) bs) p = SOME x) ==>
525 p < code_length bs``,
527 \\ `code_ptr (BC_CODE ((\x. NONE),0)) + code_length bs <= p` by
538 ``!bs m l m1 l1.
539 (WRITE_CODE (BC_CODE (m,l)) bs = BC_CODE (m1,l1)) ==>
540 !p x. (m1 p = SOME x) ==> MEM x bs \/ (
[all...]
/seL4-l4v-master/HOL4/Manual/Translations/IT/Description/
H A Dmisc.tex912 \newcommand{\holtm}{\texttt{\bs{}HOLtm}}
913 \newcommand{\holty}{\texttt{\bs{}HOLty}}
914 \newcommand{\holthm}{\texttt{\bs{}HOLthm}}
915 \paragraph{Before Starting} In order to use the munger, one must ``include'' (use the \texttt{\bs{}usepackage} command) the \texttt{holtexbasic.sty} style-file, which is found in the HOL source directory \texttt{src/TeX}.
926 \holtm{}[tt]\{P(SUC n) /\bs{} q\}
931 or something very close to it, appearing in the resulting document.\footnote{The output is a mixture of typewriter font and math-mode characters embedded in a \texttt{\bs{}texttt} block within an \texttt{\bs{}mbox}.}
949 The output is suited for inclusion in the normal flow of \LaTeX{} (it is an \texttt{\bs{}mbox}).
956 Again, the output is wrapped in an \texttt{\bs{}mbox}.
960 escaped by preceding it with a backslash~(\bs)
[all...]
/seL4-l4v-master/HOL4/examples/l3-machine-code/x64/model/
H A Dx64AssemblerLib.sml203 [(bs, "")] => ("bytes " ^ bs, NONE)
204 | [(bs, s)] => (s, SOME (bs, check c l s))
/seL4-l4v-master/HOL4/examples/machine-code/instruction-set-models/common/
H A Dbit_listScript.sml13 (bits2num (T::bs) = 1 + 2 * bits2num bs) /\
14 (bits2num (F::bs) = 0 + 2 * bits2num bs)` ;
/seL4-l4v-master/isabelle/src/Tools/Graphview/
H A Dlayout.scala103 { case (a, (content, (_, bs))) =>
107 ((Node(a), Info(0.0, 0.0, w2, h2, lines)), bs.toList.map(Node(_)))
258 val bs = if (top_down) graph.imm_preds(a) else graph.imm_succs(a)
259 bs.iterator.map(graph.get_node(_).x - x).sum / (bs.size max 1)
/seL4-l4v-master/l4v/isabelle/src/Tools/Graphview/
H A Dlayout.scala103 { case (a, (content, (_, bs))) =>
107 ((Node(a), Info(0.0, 0.0, w2, h2, lines)), bs.toList.map(Node(_)))
258 val bs = if (top_down) graph.imm_preds(a) else graph.imm_succs(a)
259 bs.iterator.map(graph.get_node(_).x - x).sum / (bs.size max 1)
/seL4-l4v-master/HOL4/examples/machine-code/instruction-set-models/x86/
H A Dx86_seq_monadScript.sml185 (let bs = word2bytes 4 w in
186 parT_unit_seq (write_mem_seq ii (a+0w) (EL 0 bs)) (parT_unit_seq (write_mem_seq ii (a+1w) (EL 1 bs))
187 (parT_unit_seq (write_mem_seq ii (a+2w) (EL 2 bs)) (write_mem_seq ii (a+3w) (EL 3 bs)))))`;

Completed in 307 milliseconds

1234